Dijkstra, Hoare
Weakest Predicate de Dijkstra : wp(S, Q) la précondition la plus faible de S par rapport à Q ; décrit tous les états initiaux tels qu'une exécution de S qui débute dans un de ces états termine OBLIGATOIREMENT dans l'état Q.
Triplet de Hoare : {P}S{Q} où P est une pré-condition, S un programme (une séquence d'instructions) et Q une post-condition.
{P}S{Q} = (P & wp(S, true) --> wp(S, Q))
Affectation
Dijkstra
P = wp(x := E, Q)
= Q[x <-- E]
Hoare
AFF1 -------------------------
{Q[x <-- E]} x := E {Q}
AFF2 --------------------------------------------
{P} x := E {P[x <-- x0] & x = E[x <-- x0]}
Exemple
P = wp(S,Q) avec
S = i := i - 1
Q = i = 0
P = wp(i := i - 1, i = 0)
= (i = 0)[i <-- i - 1]
= (i - 1 = 0)
= (i = 1)
--------------------------
{i = 1} i := i - 1 {i = 0}
Composition séquentielle
Dijkstra
P = wp(S1 ; S2, R)
= wp(S1, wp(S2, R))
Hoare
{P} S1 {Q} {Q} S2 {R}
SEQ -----------------------
{P} S1 ; S2 {R}
Exemple
P = wp(S, P) avec
S = a := 0 ; b := x
Q = a + b >= 0
P = wp(a:= 0 ; b := x, a + b >= 0)
= wp(a := 0, wp(b := x, a + b >= 0) = wp(a := 0, (a + b >= 0)[b <-- x])
= wp(a := 0, a + x >= 0) = (a + x >= 0)[a <-- 0]
= (0 + x >= 0)
AFF1 -------------------------------- -------------------------------- AFF1
{0 + x >= 0} a := 0 {a + x >= 0} {a + x >= 0} b := x {a + b >= 0}
SEQ -------------------------------------------------------------------
{0 + x >= 0} a := 0 ; b := x {a + b >= 0}
Règle de conséquence
Hoare
P --> P' {P'} C {Q'} Q' --> Q
CONSEQ -------------------------------
{P} C {Q}
Exemple
Prouver la correction du triplet {P}S{Q} avec
P = x >= 0
S = a := 0 ; b := x
Q = a >= -b
AFF1 -------------------------------- -------------------------------- AFF1
{0 + x >= 0} a := 0 {a + x >= 0} {a + x >= 0} b := x {a + b >= 0}
SEQ ------------------------------------------------------------------
x >= 0 --> 0 + x >= 0 {0 + x >= 0} a := 0 ; b := x {a + b >= 0} a + b >= 0 --> a >= -b
CONSEQ --------------------------------------------------------------------------------------
{x >= 0} a := 0 ; b := x {a >= -b}
On peut vérifier P --> P' avec
P' = wp(S, Q)
P' = wp(S, Q)
= wp(a := 0 ; b := x, a >= -b)
= wp(a := 0, wp(b := x, a >= -b)) = wp(a := 0, (a >= -b)[b <-- x])
= wp(a := 0, a >= -x) = (a >= -x)[a <-- 0]
= (0 >= -x)
P --> P' = (0 >= -x --> x >=0) = true
Instruction conditionnelle
Dijkstra
P = wp(if B then S1 else S2, Q)
= B --> wp(S1, Q) & ~P --> wp(S2, Q)
Hoare
{P & B} S1 {Q} {P & ~B} S2 {Q}
COND ---------------------------------
{P} if B then S1 else S2 {Q}
Exemple
P = wp(S, Q) avec
S = if y = 0 then x := y else x := 0
Q = x = 0
P = wp(if y = 0 then x := y else x := 0, x = 0)
= (y = 0 -> wp(x := y, x = 0)) & (~(y = 0) --> wp(x := 0, x = 0))
= (y = 0 --> 0 = Y) & (~(y = 0) --> 0 = 0)
= true & &true
= true
---------------------------------------------------- AFF1
(true & ~(y = 0)) --> (0 = 0) {0 = 0} x := 0 {x = 0}
AFF1 ----------------------------- ---------------------------------------------------- CONSEQ
{true & y = 0} x := y {x = 0} {true & ~(y = 0)} x := 0 {x = 0}
COND ---------------------------------------------------------------------------
{true} if y = 0 then x := y else x := 0 {x = 0}
Boucles
Hoare
{P & B} S {P}
WHILE --------------------------------
{P} while B do S done {P & ~B}
Note : Cette règle de correction partielle ne garantit pas la terminaison de S (cf. Correction totale).
Exemple
-------------------------------- AFF
(x >= 0 & x < b) --> x + 1 >= 0 {x + 1 >= 0} x := x + 1 {x >= 0}
CONSEQ -----------------------------------------------------------------
{x >= 0 & x < b} x := x + 1 {x >= 0}
WHILE ----------------------------------------------------------------
{x >= 0} while x < b do x := x + 1 done {x >= 0 & ~(x < b)}
Correction totale
Dijkstra
P = wp(while B do S end, Q)
P(0) = ~B & Q S n'est pas exécuté
P(1) = B & wp(S, P(0)) S est exécuté une fois et après Q est établie
...
P(k) = B & wp(S, P(k - 1))
et donc
P = wp(while B do S end, Q) = 'E'k >= 0 : P(k)
Hoare
{P & B & (E = n)} C {P & E < n & E >= 0}
WHILET ------------------------------------------
{P} while B do C done {P & ~B}
Crédit image : Wikipedia, http://en.wikipedia.org/wiki/Hoare_logic
