Correttezza - imperativo Flashcards
Correttezza - imperativo
Cosa si intende per correttezza di un programma
La correttezza di un programma è un concetto che si lega strettamente alla domanda “qual è il significato di un programma?”: infatti prima di tutto dobbiamo essere in grado di descrivere precisamente e formalmente un programma, per essere in grado di provare che fa quello che dovrebbe fare.
Correttezza - imperativo
Metodo delle invarianti
La correttezza di un programma si può esprimere come una frase che enuncia il contenuto di una certa variabile. è faciel tener traccia della verità di queste frasi quando si tratta di semplici assegnazioni di variabili, diventa complicato quando ci sono i loop: non c’è un modo semplice e genrale per dire quanti loop saranno eseguiti e quindi predirre la verità di queste frasi.
Una possibile soluzione è di provare a trovare una proprietà sugli effetti del loop che sia vera a prescindere da quanti loop vengono eseguiti.
Una “loop invariant” è una frase che è vera alla fine di un loop, sotto l’ipotesi che fosse vera all’inizio (la sua veridicità non è affetta dall’esecuzione del loop).
Correttezza - imperativo
Logica hoare
è una semantica assiomatica di Imp.
M,N sono espressioni numeriche;
A,B sono espressioni booleane;
p sono programmi;
M, N ::= 0 | 1 | . . . | x | M + N
A, B ::= true | false | A => B | M < N | M = N
p ::= skip | p; q | x := M | if B then p else q | while B do p
Correttezza - imperativo
Not A
Logica di hoare
A => false
Correttezza - imperativo
A or B
Logica di hoare
not(A)=>B
Correttezza - imperativo
A and B
Logica di hoare
not(not(A) or not(B))
not(A=>not(B))
Correttezza - imperativo
M>=N
Logica di hoare
not(M<N)
Correttezza - imperativo
Cos’è una formula
è una proposizione o una tripla:
Form ::= Prop | {Prop} Com {Prop}
La proposizione P e Q nella formula {P} C {Q} sono chiamat rispettivamente precondizione e postcondizione. Il significato intuitivo della tripla è: “se P è vero prima dell’esecuzione del programma C, allora Q è vera dopo che C termina, se termina”.
Questa interpretazione delle triple di Hoare è chiamata correttezza parziale, poiché la postcondizione è destinata a valere a condizione che C termini.
Correttezza - imperativo
True
Regole generali
true
La regola true è una postcondizione banale di qualsiasi programma.
Correttezza - imperativo
False
Regole generali
false
La regola false è una precondizione banale di qualsiasi programma.
Correttezza - imperativo
Str
Regole generali
str
Permette di rafforzare (strenthen) la precondizione di una formula
Correttezza - imperativo
Weak
Regole generali
weak
Permette di diminuire (weaken) la postcondizione di una formula.
Correttezza - imperativo
Skip
Regole speciali
skip
Skip non cambia il mondo: ciò che era vero prima skip è vero anche dopo
Correttezza - imperativo
Assign
Regole generali
assign
Dat auna proposizione P, scriviamo [E/x]P la proposizione ottenuta sostituendo le occorrenze di x in P con E.
Per esempio se P è la proposizione y = x + 7 e E è l’espressione x + 1, allora [E/x]P è la proposizione y = x + 1 + 7. Se y = x + 1 + 7 allora, fopo l’assegnamento x:=x+1 avremo y=x+7
Correttezza - imperativo
While
Regole generali
Correttezza - imperativo
Comp
Regole generali
Correttezza - imperativo
If
Regole generali
Derivare la tripla {x = 1} x := x + 1 {x = 2}
usando str e assign
{x = 1} => {x+1=2} {x+1=2} x := x + 1 {x = 2}
Derivare la tripla
{x >= 0, y > 0}x = x + y{x > 0}
{x >= 0, y > 0} => {x+y > 0} {x+y > 0} x = x + y {x > 0}
