Master d’informatique 2007 2008 de l’université Paris VI
cps
Exercice corrigé logique de Hoare / Tableaux

On souhaite démontrer que la spécification suivante est correcte :

{ A.len=B.len /\ A.len>=0 }   (P)
i = 0;
while(i<A.len) {
 B[i] = k*A[i];
 i = i + 1;
}
{ A.len=B.len /\ A.len>=0 /\ forall 0<=j<A.len, B[j] = k*A[j] }    (Q)

- on cherche l’invariant I de la boucle

Candidat :

  I = forall 0<=j<i, B[j]=k*A[j]  /\ i>=0 /\ i<=A.len
       /\ A.len=B.len /\ A.len>=0

- on montre I/\not(S) ==> Q (sortie de boucle)

[1] I/\ i>=A.len  <==>  forall 0<=j<i, B[j]=k*A[j]  /\ i>=0 /\ i=A.len
                       /\ A.len=B.len /\ A.len>=0
                  ==>  A.len=B.len /\ A.len>=0 /\ forall 0<=j<A.len, B[j]=k*A[j]

(c’est même équivalent, donc la postcondition donnée est la plus forte possible)

- on fait remonter I le long de la boucle

[2] {forall 0<=j<i+1, B[j]=k*A[j] /\ i+1>=0 /\ i+1<=A.len } i = i + 1 { I }  (aff)
    /\ A.len=B.len /\ A.len >=0    (I')
[3] {forall 0<=j<i+1 B(i<-k*A[i])[j]=k*A[j] /\ i+1>=0 /\ i+1<=A.len} B[i] = k*A[i] {I'} (tab)
    /\ A.len=B.len /\ A.len >=0    (I'')

rappel : pour tout tableau T ,

  si d=expr2 alors T(expr2<-expr1)[d]=expr1
 pour tout d<>expr2 alors T(expr2<-expr1)[d]=T[d]

On en déduit

I'' <==>  forall 0<=j<i B[j]=k*A[j] /\ k*A[i]=k*A[i] /\ i+1>=0 /\ i+1<=A.len
                      /\ A.len=B.len /\ A.len >=0
                <==>   forall 0<=j<i B[j]=k*A[j] /\ i+1>=0 /\ i+1<=A.len
                      /\ A.len=B.len /\ A.len >=0
[4] {I''}  B[i] = k*A[i] {I}  (seq)
[5] {I''}  B[i] = k*A[i] {I}  (let)

- on montre I/\S ==> I’’ (entrée dans la boucle)

[6] forall 0<=j<i, B[j]=k*A[j]  /\ i>=0 /\ i<=A.len /\ A.len=B.len /\ A.len>=0
   /\ i<A.len
   <==> forall 0<=j<i, B[j]=k*A[j]  /\ i>=0 /\ i<A.len /\ A.len=B.len /\ A.len>=0
   ===> forall 0<=j<i B[j]=k*A[j] /\ i+1>=0 /\ i+1<=A.len /\ A.len=B.len /\ A.len >=0
   (ok, car i>=1 ==> i+1>=0  et  i<A.len ==> i+1<=A.len)

- conclusion pour la boucle

[7] {I} while .... {Q}  (while [6] [5] [1])
[8] {forall 0<=j<0, B[j]=k*A[j]  /\ 0>=0 /\ 0<=A.len } i=0  {I}  (aff)
    /\ A.len=B.len /\ A.len>=0
    <==> true /\ true /\ true /\ A.len=B.len /\ A.len>=0
    <==> A.len=B.len /\ A.len>=0 <==> P
[9] {P} i=0 ; while .... {Q} (seq [8][7])

cqfd.