Metodi formali nello sviluppo software
a.a.2013/2014
Prof. Anna Labella
12/19/2015
1
Logica di Hoare (correttezza parziale)
Asserzione induttiva
{P} S {Q}

{P} skip {P}

{false} abort {P}

{P1} S {P2} {P2} S’ {P3}
{P1} S ; S’ {P3}

{PC} S1 {Q} {P¬ C} S2 {Q}
{P} if C then S1 else S2 {Q}

{IC} S {I}
.
{I} while C do S {I¬C}
12/19/2015
2
Logica di Hoare

P’ P {P} S {Q} Q  Q’
{P’} S {Q’}

{[xE] P} x:=E

correttezza totale

{P}
{IC  0≤v=V} S {I  0≤v<V}
{I 0≤v} while C do S {I¬C}
12/19/2015
3
Minima precondizione
A B significa che A è più forte di B
(perché “non necessariamente vera” quanto B)
Dato {P} S {Q} possiamo calcolarci
la minima precondizione [S]Q (trasformatore di predicato)
Vale:
{P} S {Q}  P[S]Q
12/19/2015
4
Minima precondizione
•[skip]Q = Q
•[abort]Q = false
•[x:= E]Q = [x:= E] Q
•[S;S’] Q = [S][S’]Q
•[if B then S1 else S2] Q = (B  [S1] Q ) (B  [S2] Q)
•[while B do S] Q = ( B  Q )(B  [S; while B do S] Q)
12/19/2015
5
Semantica della logica di Hoare
Definiamo
|= {P} S {Q}
S partendo da uno stato in cui vale P,
porta in uno stato nel quale vale Q
v. Ben Ari, Huth Ryan cap.4
[S]Q è goduta dal più grande insieme di stati
dai quali, applicando S, si ottengono stati nei quali vale Q
Indichiamo wp (S,Q) con l’insieme di questi stati; spesso
Identificheremo le due cose pensando wp (S,Q) come una formula
12/19/2015
6
Alcuni teoremi
12/19/2015
7
Alcuni teoremi
12/19/2015
8
Alcuni teoremi
12/19/2015
9
Alcuni teoremi
12/19/2015
10
Alcuni teoremi
12/19/2015
11
Correttezza della logica di Hoare
Se |- HL {P} S {Q} allora |= {P} S {Q}
Equivalentemente
Se |- HL {P} S {Q} allora |= P wp(S,Q)
12/19/2015
12
Correttezza della logica di Hoare
Osservazione: il ciclo
W = while B do S
può essere definito induttivamente
W° = if B then abort else skip
Wk+1 = if B then S; Wk else skip
12/19/2015
13
Correttezza della logica di Hoare
Lemma
wp (W°,Q)  B  (B  Q)
Dim:
wp (W°,Q)
=
wp ( if B then abort else skip,Q)
=
(B  wp (abort,Q)) (B  wp (skip,Q)) =
(B  false) (B  Q)

B  (B  Q)
12/19/2015
14
Correttezza della logica di Hoare
12/19/2015
15
Correttezza della logica di Hoare
Lemma

wp (Wk,Q)  wp (W,Q)
k=0,∞
Per induzione su k mostriamo
wp (Wk,Q)  wp (W,Q)
k=0
wp (W°,Q)  B  (B  Q)  B  Q
wp (W°,Q)  (B  Q) (B  wp (S;W,Q))
wp (W°,Q)  wp (W,Q)
12/19/2015
16
Correttezza della logica di Hoare
k>0
wp (Wk+1,Q) = wp ( if B then S; Wk else skip,Q)
wp (Wk+1,Q) = (B  wp (S; Wk,Q))  ( B  wp(skip,Q))
wp (Wk+1,Q) = (B  wp(S, wp(Wk,Q))(B  Q)
wp (Wk+1,Q)  (B  wp(S, wp(W,Q)))(B  Q)
wp (Wk+1,Q)  (B  wp(S;W,Q))(B  Q)
wp (Wk+1,Q)  wp (W,Q)
12/19/2015
17
Correttezza della logica di Hoare
Il caso della concatenazione
Se |- HL {P} S1; S2 {Q} allora |= P wp(S1; S2,Q)
{P}
S1 {R} {R} S2 {Q}
{P } S1 ; S2 {Q}
Per ipotesi induttiva
|= {P} S1 {R} cioè |= P  wp(S1,R)
|= {R} S2 {Q} cioè |= R wp(S2,Q)
Per monotonia
|= P  wp(S1, wp(S2,Q) )
|= P wp(S1; S2,Q)
12/19/2015
18
Correttezza della logica di Hoare
12/19/2015
19
Completezza della logica di Hoare
Se |= {P} S {Q} allora |- HL {P} S {Q}
Equivalentemente
Se |= P wp(S,Q) allora |- HL {P} S {Q}
12/19/2015
20
Completezza della logica di Hoare
Se |= P wp(S,Q) allora |- HL {P} S {Q}
12/19/2015
21
Completezza della logica di Hoare
Se |= P wp(S,Q) allora |- HL {P} S {Q}
12/19/2015
22