Correttezza - imperativo

Question 1

Correttezza - imperativo

Cosa si intende per correttezza di un programma

Answer 1

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.

Question 2

Correttezza - imperativo

Metodo delle invarianti

Answer 2

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).

Question 3

Correttezza - imperativo

Logica hoare

Answer 3

è 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

Question 4

Correttezza - imperativo

Not A

Logica di hoare

Answer 4

A => false

Question 5

Correttezza - imperativo

A or B

Logica di hoare

Answer 5

not(A)=>B

Question 6

Correttezza - imperativo

A and B

Logica di hoare

Answer 6

not(not(A) or not(B))
not(A=>not(B))

Question 7

Correttezza - imperativo

M>=N

Logica di hoare

Answer 7

not(M<N)

Question 8

Correttezza - imperativo

Cos’è una formula

Answer 8

è 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.

Question 9

Correttezza - imperativo

True

Regole generali

Answer 9

true
La regola true è una postcondizione banale di qualsiasi programma.

Question 10

Correttezza - imperativo

False

Regole generali

Answer 10

false
La regola false è una precondizione banale di qualsiasi programma.

Question 11

Correttezza - imperativo

Str

Regole generali

Answer 11

str
Permette di rafforzare (strenthen) la precondizione di una formula

Question 12

Correttezza - imperativo

Weak

Regole generali

Answer 12

weak
Permette di diminuire (weaken) la postcondizione di una formula.

Question 13

Correttezza - imperativo

And

Regole generali

Answer 13

and

Question 14

Correttezza - imperativo

Or

Regole generali

Answer 14

or

Question 15

Correttezza - imperativo

Skip

Regole speciali

Answer 15

skip
Skip non cambia il mondo: ciò che era vero prima skip è vero anche dopo

Question 16

Correttezza - imperativo

Assign

Regole generali

Answer 16

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

Question 17

Correttezza - imperativo

While

Regole generali

Answer 17

while

Question 18

Correttezza - imperativo

Comp

Regole generali

Answer 18

comp

Question 19

Correttezza - imperativo

If

Regole generali

Answer 19

if

Question 20

Derivare la tripla {x = 1} x := x + 1 {x = 2}

Answer 20

usando str e assign
{x = 1} => {x+1=2} {x+1=2} x := x + 1 {x = 2}

Question 21

Derivare la tripla
{x >= 0, y > 0}x = x + y{x > 0}

Answer 21

{x >= 0, y > 0} => {x+y > 0} {x+y > 0} x = x + y {x > 0}