Winzipedia: wiki di vincenzomanzoni.com | Informatica3 / VerificaProgrammi

Informatica3.VerificaProgrammi Versioni

Nascondi le modifiche minori - Mostra le modifiche

02/08/2006 ore 23:20 CEST di Vincenzo -

Modificate le linee 2-4: da:

'''~~Autori~~:''' [[Profiles.AlbertoConsonni | Alberto Consonni]]\\
'''Hanno contribuito:'''

'''Autore:''' [[Profiles.AlbertoConsonni | Alberto Consonni]]

Ripristina

13/06/2006 ore 23:58 CEST di Vincenzo - Sostituzione del contenuto con un allegato pdf

Modificate le linee 8-114: da:

!!Introduzione

WHILE PROGRAMS: sottoinsieme di programmi, sono semplici.

Assegnamento: y:=t // diverso dall'uguale di confronto...
Composizione: s1, s2 // con s1 e s2 istruzioni

WHILE e DO s OD

Solo VARIABILI INTERE. Non ci sono oggetti, puntatori, stringhe, metodi...

S: while program, P: precondizione, Q: postcondizione

P, Q asserzioni

Esempio:
P: {TRUE}
S: m:=0
if x>y THEN m:=x ELSE m=y
Q: {m=max(x,y)}

Idea: spezzare la dimostrazione in sotto-dimostrazione

{P} S {Q} piccoli passi, ad ogni passo applico una regola (assiomi)

ASSEGNAMENTO: {P[y-->t]}y:=t {P} (da ricordare!!!!)
- all'indietro:
{0>=0(true)} x(y):=0(t) {x>=0(P)}
{u+1>3(u>2)} x(y):=u+1(t) {x>3(P)}
{x>=5(2x>=10)} y(y):=2*x(t) {y>=10(P)}
{y=5} y(y):=y+5(t) {y=10(P)}
{6>10(false)} x(y):=6(t) {x>10(P)}

- in avanti:
{P} y:=t {?} P[y-->y'] and t[y-->y'] = y
Esempi:
{y>5} y:=2*(y+5) {y'>5 and y=2*(y'+5)} --> {y>20}

COMPOSIZIONE: {P} S1 {R} (A1) , {R} S2 {Q} (A2)
{P} S1 ; S2 {Q} (A)

se vuoi provare A, --> dimostra A1 e A2
se vale A1 e A2 allora vale A

Esempi:
1) Voglio dimostrare che:
{x=y+1} x:=x+1; y:=y+2 {x=y}

A2: {x=y+2} y:=y+2 {x=y} applico regola dell'assegnamento
A1 {x+1=y+2} x=x+1 {x=y+2} applico regola dell'assegnamento
{x=y+1}
A2 e A1 implica A per via della regola di composizione

2)Voglio dimostrare che:
x>2 {x>2} P
y:= 3*x+1, x:=y+3 {x>10}
{y>7} x:=y+3 {x>10} regola assegnamento A2
{3*x+1>7} y:= 3*x+1 {y>7} regola assegnamento A1
x>10 {x>10} Q

3)
{x>=0} x:=x+1 {x>=0}
+forte
{x>=-1} x:=x+1 {x>=0} --> Regola Assegnamento
R-->P {x>=0} --> {x>=-1} conseguenza

CONSEGUENZA: R-->P {P} S {Q}
{R} S {Q}

{P} S {Q} Q-->R
{P} S {R}

FALSE --> TRUE {TRUE} S {Q}

IF THEN ELSE: {P and e} S1 {Q}, {P and not e} S2 {Q}
{P} IF e THEN S1 ELSE S2 FI {Q}

Esempi:
{y>1}(P) if(x>0)(e) then y:=y-1;(S1) else y:=y+1(S2) {y>0(Q)}

{P and e} S1 {Q}
1.{y>1} y:=y-1 {y>0} ASSEGNAMENTO
2.{y>1 and x>0} --> {y>1} LOGICA
3.{y>1 and x>0} y:=y-1 {y>0} RAFFORZAMENTO PRE 1 e 2
4.{y>-1} y:=y+1 {y>0} ASSEGNAMENTO
5.{y>1 and x<=0} --> {y>-1} LOGICA
6.{y>1and x<=0} y:=y+1 {y>0} RAFFORZAMENTO PRE 4 e 5
7.3, 6 con la regola IF THEN ELSE

{TRUE} if x>0 m:=x else m:=-x fi {m>0}

1){x>=0} m:=x {m>=0} assegnamento
2){x>0} --> {x>=0} logica
3){TRUE and x>0} --> {x>=0} logica
4){TRUE and x>0} m:=x {m>=0} rafforzamento precondizione 1,3
5){x<0} m:=-x {m>=0} assegnamento
6){TRUE and not (x>0)} --> {x<=0} logica
7){TRUE and not (x>0)} m:=x {m>=0} rafforzamento precondizione 5,6
8){TRUE} if.... {m>=0} regola if 4,7

[[(Attach:)VerificaProgrammi.pdf]]

Ripristina

13/06/2006 ore 17:24 CEST di Vincenzo - Ortografia

Modificata la linea 1: da:

!Verifica formale di programmi (semantica assiomatica~~)ASSIOMATICA~~)

!Verifica formale di programmi (semantica assiomatica)

Ripristina

13/06/2006 ore 17:23 CEST di Vincenzo - Parziale riformattazione

Modificate le linee 1-2: da:

!~~Titolo dell'articolo VERIFICA FORMALE DI PROGRAMMI (SEMANTICA ASSIOMATICA~~)
'''Autori:'''\\

!Verifica formale di programmi (semantica assiomatica)ASSIOMATICA)
'''Autori:''' [[Profiles.AlbertoConsonni | Alberto Consonni]]\\

Modificate le linee 6-12: da:

->[-~~Contenuto del sommario~~.-]

!!Sezione
Contenuto della sezione.

--> dimostrare che i programmi ~~sono corretti! Nel senso matematico, diverso dal~~ testing

->[-Appunti sulla verifica formale di programmi.-]

!!Introduzione
L'obiettivo della verifica formale dei programmi ''dimostrare che i programmi sono corretti''. Nel senso matematico, diverso dal testing.

Modificate le linee 12-13: da:

Assegnamento: y:=t //diverso dall'uguale di confronto...

Assegnamento: y:=t // diverso dall'uguale di confronto...

Modificate le linee 114-117: da:

8){TRUE} if.... {m>=0} regola if 4,7

!!!Sottosezione
Contenuto della sottosezione

8){TRUE} if.... {m>=0} regola if 4,7

Ripristina

13/06/2006 ore 15:41 CEST di AlbertoConsonni -

Ripristina

13/06/2006 ore 15:30 CEST di AlbertoConsonni -

Modificate le linee 11-12: da:

~~Attach:file.ext~~--> dimostrare che i programmi sono corretti! Nel senso matematico, diverso dal testing

--> dimostrare che i programmi sono corretti! Nel senso matematico, diverso dal testing

Modificata la linea 118: da:

Contenuto della ~~sottosezione.Attach:Attach:C:\Documents and Settings\Alberto\Documenti\\Laurea Specialistica\ Anno\ Semestre\Informatica III\VerificaProgrammi.odt~~

Contenuto della sottosezione

Ripristina

13/06/2006 ore 15:27 CEST di AlbertoConsonni -

Aggiunte le linee 1-118:

!Titolo dell'articolo VERIFICA FORMALE DI PROGRAMMI (SEMANTICA ASSIOMATICA)
'''Autori:'''\\
'''Hanno contribuito:'''

->'''Sommario'''
->[-Contenuto del sommario.-]

!!Sezione
Contenuto della sezione.

Attach:file.ext--> dimostrare che i programmi sono corretti! Nel senso matematico, diverso dal testing

WHILE PROGRAMS: sottoinsieme di programmi, sono semplici.
Assegnamento: y:=t //diverso dall'uguale di confronto...
Composizione: s1, s2 // con s1 e s2 istruzioni

WHILE e DO s OD

Solo VARIABILI INTERE. Non ci sono oggetti, puntatori, stringhe, metodi...

S: while program, P: precondizione, Q: postcondizione

P, Q asserzioni

Esempio:
P: {TRUE}
S: m:=0
if x>y THEN m:=x ELSE m=y
Q: {m=max(x,y)}

Idea: spezzare la dimostrazione in sotto-dimostrazione

{P} S {Q} piccoli passi, ad ogni passo applico una regola (assiomi)

ASSEGNAMENTO: {P[y-->t]}y:=t {P} (da ricordare!!!!)
- all'indietro:
{0>=0(true)} x(y):=0(t) {x>=0(P)}
{u+1>3(u>2)} x(y):=u+1(t) {x>3(P)}
{x>=5(2x>=10)} y(y):=2*x(t) {y>=10(P)}
{y=5} y(y):=y+5(t) {y=10(P)}
{6>10(false)} x(y):=6(t) {x>10(P)}

- in avanti:
{P} y:=t {?} P[y-->y'] and t[y-->y'] = y
Esempi:
{y>5} y:=2*(y+5) {y'>5 and y=2*(y'+5)} --> {y>20}

COMPOSIZIONE: {P} S1 {R} (A1) , {R} S2 {Q} (A2)
{P} S1 ; S2 {Q} (A)

se vuoi provare A, --> dimostra A1 e A2
se vale A1 e A2 allora vale A

Esempi:
1) Voglio dimostrare che:
{x=y+1} x:=x+1; y:=y+2 {x=y}

A2: {x=y+2} y:=y+2 {x=y} applico regola dell'assegnamento
A1 {x+1=y+2} x=x+1 {x=y+2} applico regola dell'assegnamento
{x=y+1}
A2 e A1 implica A per via della regola di composizione

2)Voglio dimostrare che:
x>2 {x>2} P
y:= 3*x+1, x:=y+3 {x>10}
{y>7} x:=y+3 {x>10} regola assegnamento A2
{3*x+1>7} y:= 3*x+1 {y>7} regola assegnamento A1
x>10 {x>10} Q

3)
{x>=0} x:=x+1 {x>=0}
+forte
{x>=-1} x:=x+1 {x>=0} --> Regola Assegnamento
R-->P {x>=0} --> {x>=-1} conseguenza

CONSEGUENZA: R-->P {P} S {Q}
{R} S {Q}

{P} S {Q} Q-->R
{P} S {R}

FALSE --> TRUE {TRUE} S {Q}

IF THEN ELSE: {P and e} S1 {Q}, {P and not e} S2 {Q}
{P} IF e THEN S1 ELSE S2 FI {Q}

Esempi:
{y>1}(P) if(x>0)(e) then y:=y-1;(S1) else y:=y+1(S2) {y>0(Q)}

{P and e} S1 {Q}
1.{y>1} y:=y-1 {y>0} ASSEGNAMENTO
2.{y>1 and x>0} --> {y>1} LOGICA
3.{y>1 and x>0} y:=y-1 {y>0} RAFFORZAMENTO PRE 1 e 2
4.{y>-1} y:=y+1 {y>0} ASSEGNAMENTO
5.{y>1 and x<=0} --> {y>-1} LOGICA
6.{y>1and x<=0} y:=y+1 {y>0} RAFFORZAMENTO PRE 4 e 5
7.3, 6 con la regola IF THEN ELSE

{TRUE} if x>0 m:=x else m:=-x fi {m>0}

1){x>=0} m:=x {m>=0} assegnamento
2){x>0} --> {x>=0} logica
3){TRUE and x>0} --> {x>=0} logica
4){TRUE and x>0} m:=x {m>=0} rafforzamento precondizione 1,3
5){x<0} m:=-x {m>=0} assegnamento
6){TRUE and not (x>0)} --> {x<=0} logica
7){TRUE and not (x>0)} m:=x {m>=0} rafforzamento precondizione 5,6
8){TRUE} if.... {m>=0} regola if 4,7

!!!Sottosezione

Ripristina