Université Pierre & Marie Curie Maîtrise d'informatiqueSpécification et certification du logicielInterrogation écrite5 novembre 2001

Université Pierre & Marie Curie Maîtrise d'informatique

Spécification et certification du logiciel
Interrogation en plus
décembre 2001

On utilisera et étendra la sorte listde spécification :

Sort:listUses:elt, boolSymbols: nil :® list cons : elt, list® list mem : elt, list® boolAxioms: "xs:list; x, y:elt [A1] (mem x nil) =false [A2] (mem x (cons x xs)) =true [A3] (x¹y) Þ (mem y (cons x xs)) = (mem y xs)

Question 1

Spécifiez, en étendant la sorte list, un opérateur binaire nocctel que si xest un élément de sorte eltet xsune liste alors (nocc x xs)est le nombre d'occurences de xdans xs.

Réponse 1

Extends:listUses:intSymbols: nocc: elt, list® intAxioms: "xs:list; x, y:elt [A4] (nocc x nil) =0 [A5] (nocc x (conx x xs)) =1 + (nocc x xs) [A6] (x¹y) Þ (nocc x (cons y xs)) = (nocc x xs)

Question 2

Montrer que

pour tout x:elt, pour tout xs:list,si (nocc x xs)= 0alors (mem x xs) = false
pour tout x:elt, pour tout xs:list,si (nocc x xs)> 0alors (mem x xs) = true

Réponse 2.1

On montre par récurence sur xsque (nocc x xs) = 0 Þ (mem x xs) = false

si xs = nil, par [A4] et [A1] , il faut montrer que 0 = 0 Þ false = false. Ce qui est immédiat.
si xs = (cons y ys), notre hypothèse de récurence est (nocc x ys) = 0 Þ (mem x ys) = false, montrons

(nocc x (cons y ys)) = 0 Þ (mem x (cons y ys)) = false

On raisonne par cas:
- si x = y, par [A5] , on a que (nocc x (cons y ys))= 1 + (nocc x ys). Comme 1 + (nocc x ys) = 0est faux, l'implication
  
  1 + (nocc x ys) = 0 Þ (mem x (cons y ys)) = false
  est trivialement vraie.
- si x ¹ y, par [A3] et [A6] , la formule àmontrer devient
  
  (nocc x ys) = 0 Þ (mem x ys) = false
  ce qui est exactement notre hypothèse de récurence.

Réponse 2.2

On montre par récurence sur xsque (nocc x xs) > 0 Þ (mem x xs) = true

si xs = nil, par [A4] , on a (nocc x nil) =0. Donc (nocc x xs) > 0est faux, ce qui rend l'implication trivialement vraie.
si xs = (cons y ys), notre hypothèse de récurence est (nocc x ys) > 0 Þ (mem x ys) = true, montrons

(nocc x (cons y ys)) > 0 Þ (mem x (cons y ys)) = true

Ici encore, on raisonne par cas :
- si x = y, en utilisant, [A2] et [A5] , la formule àmontrer devient
  
  1 + (nocc x ys) > 0 Þ true = true
  Comme 1 + (nocc x ys) > 0est vrai, l'implication est aussi vérifiée.
- sinon, par [A3] et [A6] , la formule àmontrer devient
  
  (nocc x ys) > 0 Þ (mem x ys) = true
  ce qui est exactement notre hypothèse de récurence.

Question 3

Soit la suite (a_n) telle que {

a₀	=	1
a_n+1	=	2a_n+1

.

Soit le programme Asuivant :

r := 1; i := 1; while i£ ndo r := (2*r)+1; i := i+1 done

Montrez que pour n, entier quelconque, le triplet

[rÎIN Ù iÎIN] A [r=a_n]

est valide en logique de Hoare-Floyd.

Réponse 3

Initialisation

(1) Il est facile de vérifier que

rÎIN Ù iÎIN Þ r = r Ù i = i

(2) On a (règle de l'affectation)

[ r = r Ù i = i ]r := 1[ r = 1 Ù i = i ]

(3) Par (1), (2) et renforcement de la précondition, on a

[ r ÎIN Ù i ÎIN ]r := 1[ r = 1 Ù i = i ]

(4) On a (règle de l'affectation)

[ r = 1 Ù i = i ]i := 1[ r = 1 Ù i = 1 ]

(5) Par (3), (4) et séquence, on a

[ r ÎIN Ù i ÎIN ]r := 1; i := 1[ r = 1 Ù i = 1 ]

(6) Il est facile de vérifier que

r = 1 Ù i = 1 Þ (r = a_i_-1 Ù i-1 £ n)

(7) Par affaiblissement de la postcondition sur (5) et (6), on a

[ r ÎIN Ù i ÎIN ]r := 1; i := 1[ r = a_i_-1 Ù i-1 £ n ]

Boucle

L'invariant de boucle est r = a_i_-1 Ù i-1 £ n

(8) Par affectation, on a

[ (2*r)+1 = a_i Ù i-1 £ n Ù i £ n ]r := (2*r)+1[ r = a_i Ù i-1 £ n Ù i£ n ]

(9) Il est facile de vérifier que

r = a_i_-1 Þ (2*r)+1 = a_i

(10) Par (8), (9) et renforcement de la précondition, on a

[ r = a_i_-1 Ù i-1 £ n Ù i £ n ]r := (2*r)+1[ r = a_i Ù i-1 £ n Ù i £ n ]

(11) Comme i = (i+1)-1, on a, par affectation

[ r = a_i Ù i £ n ]i := i+1[ r = a_i Ù i-1 £ n ]

(12) Par renforcement de la précondition (11), on a

[ r = a_i Ù i-1 £ n Ù i £ n ]i := i+1[ r = a_i Ù i-1 £ n ]

(13) Par séquence sur (10) et (12), on a

[ r = a_i_-1 Ù i-1 £ n Ù i £ n ]r := (2*r)+1; i := i+1[ r = a_i Ù i-1 £ n ]

(14) Par règle de la boucle sur (13), on a

[ r = a_i_-1 Ù i-1 £ n ]while i£ ndo r := (2*r)+1; i := i+1 done[ r = a_i_-1 Ù i-1 £ n Ù ¬(i £ n) ]

Conclusion

(15) Par séquence sur (7) et (14), on a

[ r ÎIN Ù i ÎIN ]r := 1; i := 1; while i£ ndo r := (2*r)+1; i := i+1 done[ r = a_i_-1 Ù i-1 £ n Ù ¬(i £ n) ]

(16) On vérifie facilement que

i-1 £ n Ù ¬(i £ n) Þ i = n+1

(17) Par renforcement de la précondition (16), on obtient donc

[ r ÎIN Ù i ÎIN ]r := 1; i := 1; while i£ ndo r := (2*r)+1; i := i+1 done[ r = a_n ]

Question 4

Soit la célèbre suite (b_n) dite de fibonacci {

b₀	=	1
b₁	=	1
b_n+2	=	b_n+ b_n+1

.

Soit le programme Bsuivant :

r1 := 1; r2 := 1; i := 2; while i£ ndo x := r2; r2 := r1 + r2; r1 := x; i := i+1 done

Montrez que pour n, entier quelconque, le triplet

[r1ÎIN Ù r2ÎIN Ù iÎIN Ù xÎIN] B [r2=a_n]

est valide en logique de Hoare-Floyd.

This document was translated from L^AT_EX by H^EV^EA.