04/11/23 1

Metodi formali nello sviluppo software

a.a.2013/2014

Prof. Anna Labella

04/11/23 2

Logica di Hoare (correttezza parziale)

{P} skip {P}

{false} abort {P}

{P1} S {P2} {P2} S’ {P3}

{P1} S ; S’ {P3}

{PC} S1 {Q} {P¬ C} S2 {Q}

{P} if C then S1 else S2 {Q} {IC} S {I} .

{I} while C do S {I¬C}

Asserzione induttiva

{P} S {Q}

04/11/23 3

Logica di Hoare

P’ P {P} S {Q} Q Q’ {P’} S {Q’}

{[xE] P} x:=E {P}

correttezza totale

{IC 0≤v=V} S {I 0≤v<V} {I 0≤v} while C do S {I¬C}

04/11/23 4

A B significa che A è più forte di B (perché “non necessariamente vera” quanto B)

Minima precondizione

Dato {P} S {Q} possiamo calcolarci la minima precondizione [S]Q (trasformatore di predicato)

Vale:{P} S {Q} P[S]Q

04/11/23 5

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)

04/11/23 6

Semantica della logica di Hoare

[S]Q è goduta dal più grande insieme di statidai 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

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

04/11/23 7

Alcuni teoremi

04/11/23 8

Alcuni teoremi

04/11/23 9

Alcuni teoremi

04/11/23 10

Alcuni teoremi

04/11/23 11

Alcuni teoremi

04/11/23 12

Correttezza della logica di Hoare

Se |- HL {P} S {Q} allora |= {P} S {Q}

EquivalentementeSe |- HL {P} S {Q} allora |= P wp(S,Q)

04/11/23 13

Correttezza della logica di Hoare

Osservazione: il ciclo

W = while B do S

può essere definito induttivamente

W° = if B then abort else skipWk+1 = if B then S; Wk else skip

04/11/23 14

Correttezza della logica di HoareLemma

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)

04/11/23 15

Correttezza della logica di Hoare

04/11/23 16

Correttezza della logica di Hoare

Lemma

k=0,∞wp (Wk,Q) wp (W,Q)

Per induzione su k mostriamowp (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)

04/11/23 17

Correttezza della logica di Hoarek>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)

04/11/23 18

Correttezza della logica di HoareIl caso della concatenazioneSe |- 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)

04/11/23 19

Correttezza della logica di Hoare

04/11/23 20

Completezza della logica di Hoare

Se |= {P} S {Q} allora |- HL {P} S {Q}

EquivalentementeSe |= P wp(S,Q) allora |- HL {P} S {Q}

04/11/23 21

Completezza della logica di HoareSe |= P wp(S,Q) allora |- HL {P} S {Q}

04/11/23 22

Completezza della logica di HoareSe |= P wp(S,Q) allora |- HL {P} S {Q}