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

Programmation
Spécification et certification du logiciel
Notes de cours

P. Manoury

2001-02

1  Spécifications algébriques

extern int getc __P ((FILE *));
extern int getchar __P ((void));
extern char* gets __P ((char*));
/* etc ... */

val read_line : unit -> string
val read_int : unit -> int
val read_float : unit -> float

Type de données abstrait

type 'a t

val create: unit -> 'a t

val push: 'a -> 'a t -> unit

val pop: 'a t -> 'a

val clear : 'a t -> unit

val length: 'a t -> int

(* This module implements stacks (LIFOs), with in-place modification. *)

type 'a t
        (* The type of stacks containing elements of type ['a]. *)

val create: unit -> 'a t
        (* Return a new stack, initially empty. *)
val push: 'a -> 'a t -> unit
        (* [push x s] adds the element [x] at the top of stack [s]. *)
val pop: 'a t -> 'a
        (* [pop s] removes and returns the topmost element in stack [s],
           or raises [Empty] if the stack is empty. *)
val clear : 'a t -> unit
        (* Discard all elements from a stack. *)
val length: 'a t -> int
        (* Return the number of elements in a stack. *)

Spécifications équationnelles

Sort: stack

Uses: int, elt

Symbols:
 create : ® stack
 push : elt, stack ® stack
 top : stack ® elt
 pop : stack ® stack
 length : stack ® int

• la première ligne qui commence par le mot clé Sort donne le nom de la sorte (type abstrait) que l'on introduit.
• la seconde ligne qui commence par Uses donne la liste des autres sortes devant intervenir dans la spécification. Ici, les entiers (sorte int) et une sorte indéterminée eltqui joue le rôle de paramètre de sorte (le 'ades types ML).
• les lignes suivantes, inroduites par Symbols donnent la listes des symboles composants la spécification avec leur sorte respective.

Axioms: " s:stack; x:elt.

 [A1] (top (push x s)) = x

 [A2] (pop (push x s)) = s

 [A3] (length create) = 0

 [A4] (length (push x s)) = 1+(length s)

• les opérateurs createet pushjouent un rôle particulier concernant les piles : celui de constructeurs. Ce sont des primitives abstraites dont aucune équation ne définit la valeur (il n'y a pas d'équation de la forme (push ...) = ...). On a de plus que toute expression de sorte stackpeut se ramener, par le jeu des èquations, àune expression utilisant uniquement createet push.
• la valeur des opérateurs topet popn'est pas spécifiée lorsqu'on les applique àune pile vide (de longueur nulle).
• l'opérateur lengthest défini par des équations récursives.

Résumé

Sort: stack

Uses: int, elt

Symbols:
 create : ® stack
 push : elt, stack ® stack
 top : stack ® elt
 pop : stack ® stack
 length : stack ® int

Axioms: " s:stack; x:elt.

 [A1] (top (push x s)) = x

 [A2] (pop (push x s)) = s

 [A3] (length create) = 0

 [A4] (length (push x s)) = 1+(length s)

Langage des spécifications algébriques (1)

Des listes

Sort: list

Uses: elt, int

Symbols:
 nil : ® list
 cons : elt, list ® list
 length : list ® int
 hd : list ® elt
 tl : list ® list
 append : list, list ® list
 rev : list -> list
 rev_append : list, list -> list


Axioms: " xs, ys:list; x:elt

 [A5] (length nil) = 0
 [A6] (length (cons x xs)) = 1+(length xs)

 [A7] (hd (cons x xs)) = x

 [A8] (tl (cons x xs)) = xs

 [A9] (append nil ys) = ys
 [A10] (append (cons x xs) ys) = (cons x (append xs ys))

 [A11] (rev nil) = nil
 [A12] (rev (cons x xs)) = (append (rev xs) (cons x nil))

 [A13] (rev_append nil ys) = ys
 [A14] (rev_append (cons x xs) ys) = (rev_append xs (cons x ys))

Theorems: " xs, ys, zs:list

 [T1] (append xs nil) = xs

 [T2] (length (append xs ys)) = (length xs) + (length ys)

 [T3] (append (append xs ys) zs) = (append xs (append ys zs))

 [T4] (rev_append xs ys) = (append (rev xs) ys)

 [T5] (rev xs) = (rev_append xs nil)

La preuve de T1

• si xs = nil, on a immédiatement (append nil nil) = nil;
• si xs = (cons x xs'), notre hypothèse de récurrence est que (append xs' nil) = xs'et il faut monter que
  
  
  (append (cons x xs') nil) = (cons x xs')
  
  on a:
  

  (append (cons x xs') nil)	=	(cons x (append xs') nil)	par définition de append
  	=	(cons x xs')	par hypothèse de récurence

La preuve de T2

• si xs = nil, on a immédiatement (length (append xs ys)) = (length ys);
• si xs = (cons x xs'), notre hypothèse de récurrence est que
  
  
  (length (append xs' ys)) = (length xs') + (length ys).
  
  on a:
  

  (length (append (cons x xs') ys))	=	1 + (length (append xs' ys))
  	=	1 + (length xs') + (length ys)
  	=	(length (cons x xs)) + (length ys)

La preuve de T3

La preuve de T4

• si xs = nil, l'égalité est immédiate;
• si xs = (cons x xs'), notre hypothèse de récurrence est que
  
  
  " ys:list. (rev_append xs' ys) = (append (rev xs') ys)
  
  Il faut montrer, pour un ys:listquelconque, que
  
  
  (rev_append (cons x xs') ys) = (append (rev (cons x xs')) ys)
  
  C'est àdire, en utilisant les axiomes équationnels et l'associativitéde append :
  
  
  (rev_append xs' (cons x ys)) = (append (rev xs') (cons x ys))
  
  Il suffit alors d'instancier le ys(quantifié) de l'hypothèse de récurrence par (cons x ys)pour obtenir l'égalité recherchée.

L'égalité T5

Équations conditionnelles

Extends: list

Symbols:
 nth : list, int ® elt

Axioms: " xs:list; x:elt; i:int

 [A15] (nth (cons x xs) 0) = x
 [A16] (0 < i), (i £ (length xs)) Þ (nth (cons x xs) i) = (nth xs (i-1))

Extends: list

Symbols:
 mem : elt, list ® bool

Axioms: " xs:list; x,y:elt

 [A17] (mem x nil) = false

 [A18] (mem x (cons x xs)) = true

 [A19] (x¹y) Þ (mem y (cons x xs)) = (mem y xs)

Listes ordonnées

Extends: list

Assume:
 (<) : elt, elt ® bool
 (£) : elt, elt ® bool

with: " e,e1,e2,e3:elt
 (e < e) = false
 (e1 < e2) Þ (e2 < e1) = false
 (e1 < e2), (e2 < e3) Þ (e1 < e3) = true
 (e1 £ e2) = (not (e2 < e1))

Symbols:
 sorted : list ® bool

Axioms: " xs:list; x,y:elt

 [A20] (sorted nil) = true
 [A21] (sorted (cons x nil)) = true
 [A22] (x £ y) Þ (sorted (cons x (cons y xs))) = (sorted (cons y xs))
 [A23] (y < x) Þ (sorted (cons x (cons y xs))) = false

Extends: list

Theorems: " x,y:elt; ys:list.

 [T6] (sorted (cons x (cons y ys))) Þ (x £ y) = true

 [T7] (sorted (cons y ys)) Þ (sorted ys) = true

• si ys = nil, on a, par définition, que (sorted nil) = true. Ce qui suffit àétablir l'implication;
• si ys = (cons z zs), on raisonne par l'absurde, en supposant que (H1) (sorted (cons x (cons z zs))) = trueet que (H2) (sorted (cons z zs)) = false.
  De H1 et de 6., on obtient que (x £ z) = true. On peut alors utiliser la définition de sorted(troisième clause) pour tirer de H1 que (sorted (cons z zs)) = true, ce qui contredit H2.

Opérateur de tri.

Extends: list

Symbols:
 ins : elt, list ® list
 ins_sort : list ® list

Axioms: " xs:list; x,y:elt

 [A24] (ins x nil) = (cons x nil)
 [A25] (x £ y) Þ (ins x (cons y xs)) = (cons x (cons y xs))
 [A26] (y < x) Þ (ins x (cons y xs)) = (cons y (ins x xs))

 [A27] (ins_sort nil) = nil
 [A28] (ins_sort (cons x xs)) = (ins (ins_sort xs))

Theorems: " xs:list

 [T8] (sorted (ins_sort xs)) = true

Le théorème de correction

Extends: list

Lemma: " xs:list; x:elt

 9. (sorted xs) Þ (sorted (ins x xs)) = true

Extends: list

Lemma: " xs:list; x,y:elt

 9.1 (x £ y), (sorted (cons x xs)) Þ (sorted (cons x (ins y xs))) = true

• si xs = nil, le résultat est immédiat.
• si xs = (cons z zs), on a les hypothèses suivantes :
  HR: " x,y:elt. (x £ y), (sorted (cons x zs)) Þ (sorted (cons x (ins y zs))) = true
  H1: (x £ y) = true
  H2: (sorted (cons x (cons z zs))) = true
  
  Notons que de H2, on tire
  H21: (x £ z) = trueet
  H22: (sorted (cons z zs)) = true
  
  Il faut montrer qu'alors: (sorted (cons x (ins y (cons z zs)))) = true.
  
  Pour cela, on raisonne par cas sur la valeur de (y £ z) :
  • si (y £ z) = true, il faut montrer que (sorted (cons x (cons y (cons z zs)))) = true. Les hypothèses nous donnent que x £ y £ zce qui permet d'obtenir le résultat recherché par application de la définiton de sorted.
  • sinon, (z < y) = trueet il faut montrer que (sorted (cons x (cons z (ins y zs)))) = true.
    En utilisant H21, il reste à montrer que (cons z (ins y zs))) = true. Notons que, comme on est dans le cas où(z < y) = true, on a aussi que H3: (z £ y) = true. On utilise alors H3 et H22 pour tirer notre résultat de l'hypothèse de récurrence HR où xest instancié en z.

Langage des spécifications algébriques (2)

Modélisation des vecteurs

Module Array: array operations

val length : 'a array -> int

      Return the length (number of elements) of the given array. 

val get: 'a array -> int -> 'a

      Array.get a n returns the element number n of array a. The first
      element has number 0. The last element has number Array.length a
      - 1. Raise Invalid_argument "Array.get" if n is outside the
      range 0 to (Array.length a - 1). You can also write a.(n)
      instead of Array.get a n.

val set: 'a array -> int -> 'a -> unit

      Array.set a n x modifies array a in place, replacing element
      number n with x. Raise Invalid_argument "Array.set" if n is
      outside the range 0 to Array.length a - 1. You can also write
      a.(n) <- x instead of Array.set a n x.

val make: int -> 'a -> 'a array
val create: int -> 'a -> 'a array

      Array.make n x returns a fresh array of length n, initialized
      with x. All the elements of this new array are initially
      physically equal to x (in the sense of the ==
      predicate). Consequently, if x is mutable, it is shared among
      all elements of the array, and modifying x through one of the
      array entries will modify all other entries at the same time.

Sort: vect

Uses: int, elt

Symbols:
 length : vect ® int
 get : vect, int ® elt
 set : vect, int, elt ® vect
 make : int, elt ® vect

Axioms: " v:vect; e:elt; n,i,j:int

 [A29] (length (make n e)) = n

 [A30] (length (set v i e)) = (length v)

 [A31] (0 £ i), (i < n) Þ (get (make n e) i) = e

 [A32] (0 £ i), (i < (length v)) Þ (get (set v i e) i) = e

 [A33] (0 £ i), (i < (length v)), (0 £ j), (j < (length v)), (i ¹ j)
    Þ (get (set v i e) j) = (get v j)

Extends: vect

Uses: bool

Symbols:
 indom : int, vect ® bool

Axioms: " v:vect; i:int

 [A34] (0 £ i), (i < (length v)) Þ (indom i v) = true

 [A35] (indom i v) Þ (0 £ i) = true

 [A36] (indom i v) Þ (i < (length v)) = true

Le plus petit indice de l'élément maximal d'un tableau

Extends: vect

Assume:
 (<) : elt, elt ® bool
 (£) : elt, elt ® bool

with: " e,e1,e2,e3:elt
 (e < e) = false
 (e1 < e2) Þ (e2 < e1) = false
 (e1 < e2), (e2 < e3) Þ (e1 < e3) = true
 (e1 £ e2) = (not (e2 < e1))

Symbols:
 imax : vect ® int
 loop : int, int, vect ® int
 find_imax : vect ® int

Axioms: " v:vect; i,m:int; e:elt

 /* Défintion de imax */
 [A37] (indom (imax v) v) = true

 [A38] (indom i v) Þ (get v i) £ (get v (imax v))

 [A39] (indom i v), ((get v (imax v)) = (get v i)) Þ (imax v) £ i

 /* Fonction de calcul: find_max */
 [A40] (loop m (length v) v) = m

 [A41] (0 £ i), (i < (length v)), (indom m v), (get(v,m) < get(v,i))
    Þ (loop m i v) = (loop i i+1 v)

 [A42] (0 £ i), (i < (length v)), (indom m v), (get(v,i) £ get(v,m))
    Þ (loop m i v) = (loop m i+1 v)

 [A43] ((length v)¹ 0) Þ (find_max v) = (loop 0 1 v)

Theorems: " v:vect

 [T9] ((length v)¹ 0) Þ (find_max v) = (imax v)

" v:vect. ((length v)¹ 0) Þ (loop 0 1 v) = (imax v)

Extends: vect

Symbols:
 bimax : int, vect ® int

Axioms: " v:vect; i,j,m:int

 [A44] (0 < i) Þ (indom (bimax i v) v) = true

 [A45] (0 £ j), (j < i) Þ (get v j) £ (get v (bimax i v))

 [A46] (0 £ j), (j < i), ((get v (bimax i v)) = (get v j))
    Þ (bimax i v) £ j

Lemma: " v:vect; i,m:int

 [T10] ((length v) ¹ 0), (0 £ i), (i £ (length v))
    Þ (loop (bimax i v) i v) = (imax v)

• si n-i=0, alors i=net on a que (loop (bimax n v) n v)=(bimax n v)=(imax v).
• sinon, posons comme hypothèse de récurrence : (loop (bimax i+1 v) i+1 v) = (imax v)(ce qui est légitime car n-(i+1)=(n-i)-1) et montrons (loop (bimax i v) i v) = (imax v).
  On raisonne alors par cas selon que (get v i) £ (get v (bimax i v))ou non.
  • si (get v i) £ get v bimax i v)alors

    (loop (bimax i v) i v)	=	(loop (bimax i v) i+1 v)
    	=	(loop (bimax i+1 v) i+1 v)
    	=	(imax v)

  • si get v (bimax i v)) < (get v i)alors

    (loop (bimax i v) i v)	=	(loop i i+1 v)
    	=	(loop (bimax i+1 v) i+1 v)
    	=	(imax v)

  
  

Préfixe d'une liste

Définition récursive

Extends: list

Symbols:
 pref : list, list ® bool

Axioms: " x, y:elt; xs1, xs2, xs: list.

 [A47] (pref nil xs) = true

 [A48] (pref (cons x xs1) (cons x xs)) = (pref xs1 xs)

 [A49] (x ¹ y) Þ (pref (cons x xs1) (cons y xs)) = false

 [A50] (pref (cons x xs1) nil) = false

Theorems: " xs1, xs2: list.

 [T11] 1 (pref xs1 (append xs1 xs2)) = true

Preuve de [T1]

• si xs1 = nil, immédiat par [A1].
  
  
• si xs1 = (cons x xs1'), HR: (pref xs1' (append xs1' xs2)) = true.
  
  On veut (pref (cons x xs1') (append (cons x xs1') xs2)) = true. C'est àdire, par [A2] et déf. append, (pref xs1' (append xs1' xs2)) = true.

Préfixe et concaténation

Extends: list

Theorems: " xs1, xs: list.

 [T2] (pref xs1 xs) Þ $ xs2:list. xs = (append xs1 xs2)

Preuve de [T2]

• si xs1 = nil, on prend xs2 = xs.
  
  
• si xs1 = (cons x xs1'),
  HR: " xs: list. (pref xs1' xs) Þ $ xs2:list. xs = (append xs1' xs2)
  
  On montre (pref (cons x xs1') xs) Þ $ xs2:list. xs = (append (cons x xs1') xs2)par cas sur xs.
  • si xs = nil, on veut (pref (cons x xs1') nil) Þ $ xs2:list. nil = (append (cons x xs1') xs2). Trivial, sachant [A4].
    
    
  • si xs = (cons y xs'), on suppose H1: (pref (cons x xs1') (cons y xs')) = trueet on veut $ xs2:list. (cons y xs') = (append (cons x xs1') xs2).
    
    Par H1 et [A3] (contrap), on a x = y. D'où, par H1 et [A2], (pref xs1' xs') = true. D'où, par HR, il existe xs2tel que xs' = (append xs1' xs2).
    
    C'est àdire, xs = (cons x xs') = (append (cons x xs1') xs2).

Calcul d'un préfixe de longueur donnée

Extends: list

Symbols:
 n_pref : nat, list ® list

Axioms: " n:nat; x:elt; xs:list.

 [A5] (n_pref 0 xs) = nil

 [A6] (n > 0) Þ (n_pref n (cons x xs)) = (cons x (n_pref (n-1) xs))

 [A7] (n_pref n nil) = nil

Theorems: " n:nat; xs:list.

 [T3] (pref (n_pref n xs) xs) = true

Preuve de [T3]

• si n = 0, immédiat par [A5] et [A1].
• si n = n'+1, HR: " xs:list. (pref (n_pref n' xs) xs) = true.
  On montre " xs:list. (pref (n_pref (n'+1) xs) xs) = truepar cas sur xs
  • si xs = nil, immédiat par [A7] et [A1].
  • si xs = (cons x xs'), on veut (pref (n_pref (n'+1) (cons x xs)) (cons x xs)) = true.
    C'est-à-dire, par [A6], (pref (cons x (n_pref n' xs') (cons x xs')) = true.
    Immédiat par [A2] et HR.

Tri par arbre binaire de recherche

Les arbres binaires

Sort: btree

Uses: elt

Symbols:
 Lf : ® btree
 Br : btree, elt, btree ® btree
 root : btree ® elt

Axioms: " x:elt; a1, a2:btree.

 [A51] (root (Br a1 x a2)) = x

Les arbres binaires de recherche

Extends: btree

Uses: elt

Assumes:

 [Ordered elt]

Symbols:
 verify : (elt, elt ® bool), elt, btree ® bool
 maximize : elt, btree ® bool
 minimize : elt, btree ® bool
 abr : btree ® bool

Axioms: " r:elt, elt ® bool; x, y:elt; a1, a2:btree.

 [A52] (verify r x Lf) = true

 [A53] (verify r x a1), (verify r x a2), (r x y) Þ (verify r x (Br y a1 a2)

 [A54] minimize = (verify £)

 [A55] maximize = (verify ³)

 [A56] (abr Lf) = true

 [A57] (abr a1), (abr a2), (maximize x a1), (minimize x a2) Þ (abr (Br a1 x a2))

Le tri

Extends: list

Uses: elt, abr

Symbols:
 ins : elt, btree ® btree
 to-abr : list ® btree
 to-list : btree ® list
 to-list-bis : btree ® list
 abr-sort : list ® list

Axioms: " x, y:elt; xs:list; a, a1, a2, a3:btree.

 [A58] (ins x a) = (Br Lf x Lf)

 [A59] (x £ y) Þ (ins x (Br a1 y a2)) = (Br (ins x a1) y a2)

 [A60] (x ³ y) Þ (ins x (Br a1 y a2)) = (Br a1 y (ins x a2))

 [A61] (to-abr nil) = Lf

 [A62] (to-abr (cons x xs)) = (ins x (to-abr xs))

 [A63] (to-list Lf) = nil

 [A64] (to-list (Br a1 x a2)) = (append (to-list a1) (cons x (to-list a2)))

 [A65] (to-list-bis Lf) = nil

 [A66] (to-list-bis (Br Lf x a2)) = (cons x (to-list-bis a2))

 [A67] (to-list-bis (Br (Br a1 x a2) y a3)) = (to-list-bis (Br a1 x (Br a2 y a3)))

Theorems " x:elt; xs:list; a:btree.

 (sorted (abr-sort xs)) = true

 (abr (to-abr xs)) = true

 (abr a) Þ (abr (ins x a))

 (abr a) Þ (sorted (to-list a))

Graphes 1

Les couples

Sort: pair

Uses: elt1, elt2

Symbols:
 mkpair : elt1, elt2 ® pair
 fst : pair ® elt1
 snd : pair ® elt2

Axioms: " x1:elt1; x2:elt2.

 [A68] (fst (mkpair x1 x2)) = x1

 [A69] (snd (mkpair x1 x2)) = x2

Theorems: " x:pair.

 (mkpair (fst x) (snd x)) = x

Listes d'associations

Extends: list

Uses: pair

Symbols:
 assoc : elt1, list ® elt2
 add-assoc : elt1, elt2, list ® list

Axioms: " x, x':elt1; y, y':elt2; ys, xys:list.

 [A70] (assoc x (cons (mkpair x y) xys)) = y

 [A71] (x ¹ x') Þ (assoc x (cons (mkpair x' y) xys)) = (assoc x xys)

 [A72] (add-assoc x y nil) = (cons (mkpair x y) nil)

 [A73] (add-assoc x y (cons (mkpair x ys) xys)) = (cons (mkpair x (cons y ys)) xys)

 [A74] (x ¹ x') Þ (add-assoc x y (cons (mkpair x' ys) xys)) = (cons (mkpair x' ys) (add-assoc x y xys))

Theorems: " x:elt1; y:alt2; xys:list.

 (mem y (assoc x (add-assoc x y xys))) = true

Liste d'adjacences

Extends: list

Uses: pair

Symbols:
 to-adj : list -> list

Axioms: "

 [A75] (to-adj nil) = nil

 [A76] (to-adj (cons (mkpair x y) xys)) = (add-assoc x y (to-adj xys))

Theorems: " x:elt1; y:elt2; g:list.

 (mem (mkpair x y) g) Þ (mem y (assoc x (to-adj g))) = true

 (mem y (assoc x (to-adj g))) Þ (mem (mkpair x y) g) = true

2  Preuve de programmes impératifs

Assertions

let find_max v =
 let m = ref 0 in
 let i = ref 1 in
  while !i < Array.lenth v do
   if v.(!m) < v.(!i) then m := i;
   incr i
  done;
  !m 
;;

let find_max v =
 let m = ref 0 in
 let i = ref 1 in
  while !i < Array.lenth v do
   if v.(!m) < v.(!i) then m := i;
   incr i
  done;
  !m (* !m = (imax v) *)
;;

let find_max v =
 let m = ref 0 in
 let i = ref 1 in 
  (* a1 : !m = (bimax !i v) *)
  while !i < Array.length v do
   (* a2 : (!i < Array.length v) & (!m = (bimax !i v)) *)
   if v.(!m) < v.(!i) then m := i;
   (* a3 : !m = (bimax !i+1 v) *)
   incr i
   (* a4 : !m = (bimax !i v) *)
  done;
  (* a5 : (!i = Array.lenth v) & (!m = (bimax !i v)) *)
  !m 
  (* a6 : !m = (imax v) *)
;;

• a6 la dernière assertion affirme la correction générale du programme. Ce devra être une conséquence des assertions précédentes;
• a1 affirme qu'avant de rentrer dans la boucle while, la propriétéd'invariance est établie;
• a2 affirme qu'àchaque nouveau passage dans la boucle, on a l'invariance;
• a3 affirme que cette propriétéest devenue vrai pour l'indice suivant. Les assertions a2et a3tiennent lieu de schéma de récurrence oùa2est l'hypothèse de récurrence.
• a4 permet de <<retrouver>> l'hypothèse de récurrence si l'on revient dans la boucle;
• a5 donne la valeurs de l'indice de parcourt en sortie de boucle et la valeur obtenue pour m. C'est de ces deux valeur que l'on déduit la validitéde a6.

Théorie axiomatique des programmes

find_max revisité

m := 0;
i := 1;
While i < (length v) do begin
 If v(m) < v(i) then m := i else SKIP;
 i := i+1
end

1. [P] C₀ [I]
2. IÙ ¬ e Þ Q
3. [IÙ e] C [I]

Preuve de correction (partielle) de find_max

1. Il faut montrer que :
   [(length v)¹0] m:=0; i:=1 [m = (bimax i v)]
   Il est facile de vérifier que 0 = (bimax 1 v) est vrai. On a donc trivialement l'implication :
   (length v)¹0 Þ 0 = (bimax 1 v)
   En utilisant la règle de renforcement de la précondition, on obtient la séquence d'initialisation avec :
   [0=(bimax 1 v)] m := 0 [m = (bimax 1 v)] et [m = (bimax 1 v)] i := 1 [m = (bimax i v)]
   cqfd
2. En utilisant les équations de bimax, on peut montrer que si i ³ (length v)alors (bimax i v) = (imax v). D'où
   m = (bimax i v) Ù ¬(i < (length v)) Þ m = (imax v)
3. Vient maintenant le gros morceau : montrer que l'invariant est conservépar le corps de la boucle. C'est àdire (en écrivant es triplets verticalement) :

   [ m = (bimax i v) Ù i < (length v)]

   If v(m) < v(i) then m := i else SKIP;i := i+1

   [ m = (bimax i v)]

   Ou encore, par les règles de la séquence et de l'affectation :

   [ m = (bimax i v) Ù i < (length v)]

   If v(m) < v(i) then m := i else SKIP;

   [ m = (bimax i+1 v)]

   i := i+1

   [ m = (bimax i v)]

   La seconde partie de la séquence est immédiate, reste àvoir :

   [ m = (bimax i v) Ù i < (length v)]

   If v(m) < v(i) then m := i else SKIP;

   [ m = (bimax i+1 v)]

   Par la règle de l'alternative, il faut montrer que (a)

   [ m = (bimax i v) Ù i < (length v) Ù v(m) < v(i)]

   m := i

   [ m = (bimax i+1 v)]

   et que (b)

   [ m = (bimax i v) Ù i < (length v) Ù v(m) ³ v(i)]

   SKIP;

   [ m = (bimax i+1 v)]

   1. de m = (bimax i v)et v(m) < v(i), on peut déduire que i = (bimax i+1 v). Et, par règle de l'affectation, on a
      [i = (bimax i+1 v)] m := i [m = (bimax i+1 v)]
      On obtient le résulat attendu par renforcement de la précondition.
   2. de m = (bimax i v)et v(m) ³ v(i), on peut déduire que m = (bimax i+1 v). On a alors le résultat attendu par la règle du SKIPet renforcement de la précondition.
   cqfd

Raffinement

• si P et Q sont des formules alors [P, Q] est une spécification.
• si S₁ et S₂ sont des spécifications alors S₁ ; S₂ est une spécification.
• si B est une formule et si S₁ et S₂ sont des spécifications alors If B then S₁ else S₂ aussi.
• si B est une formule et S une spécification alors While B do S est une spécification.
• si S est une spécification et x est une variable alors Var x. S est une spécification.
• si x est une variable et e une expression alors x := e est une spécification.
• SKIPest une spécification.

• S₁ ; S₂Ê S'₁ ; S'₂ ;
• If B then S₁ else S₂ Ê If B then S'₁ else S'₂ ;
• While B do S₁Ê While B do S'₁ ;
• Var x. S₁Ê Var x. S'₁.

Règles de raffinement

Ne rien faire (Sk)

Affectation (As)

Séquence (Sq)

Variable locale (Vr)

Soient N et M deux valeurs entières et x, y deux variables

[x=NÙ y=M, x=MÙ y=N]	Ê	{Var z . [x=NÙ y=M, y=NÙ x=M] }
	Ê	{Var z .
		[x=NÙ y=M, z=NÙ y=M] ;
		[z=NÙ y=M, y=NÙ x=M] }
	Ê	{Var z .
		z := x ;
		[z=NÙ y=M, y=NÙ x=M] }
	Ê	{Var z .
		z := x ;
		[z=NÙ y=M, z=NÙ x=M] ;
		[z=NÙ x=M, y=NÙ x=M] }
	Ê	{Var z .
		z := x ;
		x := y ;
		[z=NÙ x=M, y=NÙ x=M] }
	Ê	{Var z .
		z := x ;
		x := y ;
		y := z }

Précondition (St)

Postcondition (Wk)

Affectation bis (Ab)

Initialisation (Ai)

Conditionnelle (If)

Boucle (Wh)

Exemple

1. X=RÙ Q=0 Þ X=(Y× Q)+R
2. R£ Y Þ ¬(Y£ R)
3. X = (Y× Q) + R Þ X = (Y× (Q+1) + (R-Y)
4. Y>0Ù X = (Y× Q) + (R-Y) Ù Y £ R Ù R=n Þ X = (Y× Q) + (R-Y) Ù R-Y < n

Hoare-Floyd et le raffinement

• S₁ ; S₂= {  C₁ ; C₂ |  C₁Î S₁Ù C₂Î S₂ }
• If B then S₁ else S₂= {  If B then C₁ else C₂  |  C₁Î S₁Ù C₂Î S₂ }
• While B do S = {  While B do C  |  CÎ S  }
• Var x. S = {  Var x. C  |  CÎ S  }
• x := e = {  x := e  }
• SKIP = {  SKIP  }

Ne rien faire

on a directement [P] SKIP [P].

Affectation

on a aussi [Q[e/x]] x := e [Q].

Séquence

soit C₁ ; C₂Î [P,R] ; [R,Q], on a par définition, C₁Î [P,R] et C₂Î [R,Q]. D'où, |-[P] C₁ [R] et |-[R] C₂ [Q], et donc |-[P] C₁ ; C₂ [Q].

Variable

soit Var x. CÎ Var x. [P,Q], on a, par définition CÎ [P,Q], et donc |-[P] C [Q], par définition. On a donc |-[P] Var x.C [Q], puisque x n'apparaiît pas dans P ni dans Q.

Conditionnelle

soit If B then C₁ else C₂Î If B then [PÙ B, Q] else [PÙ ¬ B, Q]. On a, par définition que C₁Î [PÙ B, Q] et C₂Î[PÙ ¬ B,Q]. D'où|-[PÙ B] C₁ [Q] et |-[PÙ ¬ B] C₂ [Q]. Et donc |-[P] If B then C₁ else C₂ [Q].

Boucle

soit While B do CÎ While B do [PÙ BÙ n=e, PÙ e<n]. On a CÎ [PÙ BÙ n=e, PÙ e<n], c'est-à-dire |-[PÙ BÙ n=e] C [PÙ e<n]. D'où|-[P] While B do C [PÙ ¬ B].

Miroir d'une liste en impératif

(* xs = L *)
ys := nil;
(* (append (rev xs) ys) = (rev L) *)
While xs ¹ nil do
  (* xs ¹ nil Ù (append (rev xs) ys) = (rev L) *)
  ys := (cons (hd xs) ys);
  (* xs ¹ nil Ù (append (rev (tl xs)) ys) = (rev L) *)
  xs := (tl xs)
  (* (append (rev xs) ys) = (rev L) *)
done.
(* ys = (rev L) *)

Preuve par Hoare-Floyd

[ xs = L ]
ys := nil;
While xs ¹ nil do
  ys := (cons (hd xs) ys);
  xs := (tl xs)
done.
[ ys = (rev L) ]

xs = L
Þ (rev xs) = (rev L)
Þ (append (rev xs) nil) = (rev L) (par [T1] )

[ (append (rev xs) nil) = (rev L) ]
ys := nil;
While xs ¹ nil do
  ys := (cons (hd xs) ys);
  xs := (tl xs)
done.
[ ys = (rev L) ]

[ (append (rev xs) nil) = (rev L) ]
ys := nil
[ (append (rev xs) ys) = (rev L) ]

[ (append (rev xs) ys) = (rev L) ]
While xs ¹ nil do
  ys := (cons (hd xs) ys);
  xs := (tl xs)
done.
[ ys = (rev L) ]

xs = nil Ù (append (rev xs) ys) = (rev L)
Þ ys = (rev L)

[ (append (rev xs) ys) = (rev L) ]
While xs ¹ nil do
  ys := (cons (hd xs) ys);
  xs := (tl xs)
done.
[ xs = nil Ù (append (rev xs) ys) = (rev L) ]

[ xs ¹ nil Ù (append (rev xs) ys) = (rev L) ]
ys := (cons (hd xs) ys);
xs := (tl xs)
[ (append (rev xs) ys) = (rev L) ]

• xs ¹ nil Þ xs = (cons (hd xs) (tl xs)) (vient de ce que toute liste est soit nil  soit cons);
• (append (rev (cons (hd xs) (tl xs))) ys) = (append (tl xs) (cons (hd xs) ys)) (facile àvérifier).

xs ¹ nil Ù (append (rev xs) ys) = (rev L)
Þ xs ¹ nil Ù (append (tl xs) (cons (hd xs) ys)) = (rev L)

[ xs ¹ nil Ù (append (tl xs) (cons (hd xs) ys)) = (rev L) ]
ys := (cons (hd xs) ys);
xs := (tl xs)
[ (append (rev xs) ys) = (rev L) ]

[ xs ¹ nil Ù (append (tl xs) (cons (hd xs) ys)) = (rev L) ]
ys := (cons (hd xs) ys)
[ xs ¹ nil Ù (append (tl xs) ys) = (rev L) ]

[ xs ¹ nil Ù (append (tl xs) ys) = (rev L) ]
xs := (tl xs)
[ (append (rev xs) ys) = (rev L) ]

Raffinement

[ xs = L, ys = (rev L) ]

[ (rev xs) = (rev L), ys = (rev L) ]

[ (append (rev xs) nil) = (rev L), ys = (rev L) ]

[ (append (rev xs) nil) = (rev L), (append (rev xs) ys) = (rev L) ] ;
[ (append (rev xs) ys) = (rev L), ys = (rev L) ]

ys := nil;
[ (append (rev xs) ys) = (rev L), ys = (rev L) ]

ys := nil;
[ (append (rev xs) ys) = (rev L), xs = nil Ù (append (rev xs) ys) = (rev L) ]

ys := nil;
While xs ¹ nil do
  [ xs ¹ nil Ù (append (rev xs) ys) = (rev L), (append (rev xs) ys) = (rev L) ]
done.

ys := nil;
While xs ¹ nil do
  [ xs ¹ nil Ù (append (rev (tl xs)) (cons (hd xs) ys)) = (rev L),
   (append (rev xs) ys) = (rev L) ]
done.

ys := nil;
While xs ¹ nil do
  ys := (cons (hd xs) ys);
  [ xs ¹ nil Ù (append (rev (tl xs)) ys) = (rev L),
   (append (rev xs) ys) = (rev L) ]
done.

ys := nil;
While xs ¹ nil do
  ys := (cons (hd xs) ys);
  xs := (tl xs)
done.

Résumé

3  Spécification ensembliste

Langage ensembliste

Relations entre ensembles

Appartenance

Inclusion

Égalité

Constructeurs d'ensembles

Ensemble vide

Union

Intersection

Différence ensembliste

Ensemble des parties

Couples et produit cartésien

Schéma de compréhension

Relations binaires et fonctions

Fonctions

Opérations sur les relations

• restriction du domaine :

  Z <| R º {(x,y)ÎX× Y  |  xÎ ZÙ x

  R

  y }

• exclusion du domaine :
  Z <|-  R º (X \Z)<| R
• restriction du codomaine :

  R |> Z º {(x,y)ÎX× Y  |  yÎ ZÙ x

  R

  y }

• mise-à-jour (de la relation R₁ par la relation R₂) :
  R₁Å R₂º (dom(R₂)<|-  R₁)È R₂

Arithmétique

Les suites

Le langage Z

Définitions axiomatiques

Schémas d'opérations

• par inclusion : si S₁ est  

  S1

  x1:T1

  j 1

    on a  

  S2   S1 x2:T2     j 2	º	S2   x1:T1 x2:T2     j 1Ùj 2

• par conjonction : si S₂ est  

  S2

  x2:T2

  j 2

    on a  

  S1Ù S2

  x1:T1 x2:T2

  j 1Ùj 2

• etc.

Un exemple

Les données

Les opérations

Les erreurs