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

Programmation
Spécification et certification du logiciel
Notes de cours

P. Manoury

2000-01

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
 clear : 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

 (top (push x s)) = x

 (pop (push x s)) = s

 (length create) = 0

 (length (push x s)) = 1+(length s)

 (length (clear s)) = 0

• les opérateurs createet pushjouent un rôle particulier concernant les piles : celui de constructeurs. cela signifie 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éfinit par des équations récursives.

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

 (length nil) = 0
 (length (cons x xs)) = 1+(length xs)

 (hd (cons x xs)) = x

 (tl (cons x xs)) = xs

 (append nil ys) = ys
 (append (cons x xs) ys) = (cons x (append xs ys))

 (rev nil) = nil
 (rev (cons x xs)) = (append (rev xs) (cons x nil))

 (rev_append nil ys) = ys
 (rev_append (cons x xs) ys) = (rev_append xs (cons x ys))

Theorems: " xs, ys, zs:list

 1. (length (append xs ys)) = (length xs) + (length ys)

 2. (append (append xs ys) zs) = (append xs (append ys zs))

 3. (rev_append xs ys) = (append (rev xs) ys)

 4. (rev xs) = (rev_append xs nil)

• 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)

• 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)
  
  En utilisant les axiomes équationnels et 2., on obtient àmontrer :
  
  
  (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.

Équations conditionnelles

Extends: list

Symbols:
 nth : list, int ® elt

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

 (nth (cons x xs) 0) = x
 (0 < i), (i £ (length xs)) Þ (nth xs i) = (nth (tl xs) (i-1))

Extends: list

Symbols:
 mem : elt, list ® bool

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

 (mem x nil) = false

 (mem x (cons x xs)) = true

 (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) = true
 (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

 (sorted nil) = true
 (sorted (cons x nil)) = true
 (x £ y) Þ (sorted (cons x (cons y xs))) = (sorted (cons y xs))
 (y < x) Þ (sorted (cons x (cons y xs))) = false

Extends: list

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

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

 (ins x nil) = (cons x nil)
 (x £ y) Þ (ins x (cons y xs)) = (cons x (cons y xs))
 (y < x) Þ (ins x (cons y xs)) = (cons y (ins x xs))

 (ins_sort nil) = nil
 (ins_sort (cons x xs)) = (ins (ins_sort xs))

Theorems: " xs:list

 1. (sorted (ins_sort xs)) = true

Extends: list

Lemma: " xs:list; x:elt

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

Extends: list

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

 2.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 tirer notre résultat de l'hypothèse de récurrence HR où xest instancié en z.

2  Assertions

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

 (length (make n e)) = n

 (length (set v i e)) = (length v)

 (0 £ i), (i < (length v)) Þ (get (make n e) i) = e

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

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

Extends: vect

Symbols:
 indom : int, vect ® bool

Axioms: " v:vect; i:int

 (indom i v) = (and (0 £ i) (i < (length v)))

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) = true
 (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

 /* imax.1 */
 (indom (imax v) v) = true

 /* imax.2 */
 (indom i v) Þ (get v i) £ (get v (imax v))

 /* imax.3 */
 (indom i v), ((get v (imax v)) = (get v i)) Þ (imax v) £ i

 (loop m (length v) v) = m

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

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

 ((length v)¹ 0) Þ (find_max v) = (loop 0 1 v)

Theorems: " v:vect

 ((length v)¹ 0) Þ (find_max v) = (imax v)

Theorems: " 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

 (0 < i) Þ (indom (bimax i v) v) = true

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

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

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

 ((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)

  
  

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.

3  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 d'affaiblissement 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 affaiblissement 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 affaiblissement de la précondition.
   cqfd

4  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 (Wk)

Postcondition (St)

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) Ù R=n Þ X = (Y× Q) + (R-Y) Ù R-Y < n

4.1  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éfintion. On a donc |-[P] Var x.C [Q], puisque x ne 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].

5  Spécification ensembliste

Langage ensembliste

Relations binaires et fonctions

• 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₂º (R₂<|-  R1)È R₂

Arithmétique

5.0.1  Les suites

Le langage Z

Défintions 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

Redéfinitions avec gestion d'erreurs

6  La méthode B

Substitutions généralisées

Substitution simple

Substitution parallèle

Substitution préconditionnée

Substitution indéterminée

Machines abstraites

machine

cette rubrique ne contient qu'un seul élément : le nom de la machine.

sets

cette rubrique contient la déclaration des ensembles dont se servira la machine. On peut déclarer un ensemble soit comme un simple identificateur (auquel cas son contenu reste abstrait) soit par extension (comme un ensemble énuméré) Tous ces ensembles sont finis (explicitement ou implicitement)

variables

cette rubrique contient la déclaration des variables qu'utilise la machine. L'ensemble de ces variables constitue l'état interne de la machine.

invariant

cette rubrique contient une formule. C'est un élément trés important de la spécification. L'invariant contient la propriétéglobale que doit satisfaire la machine. Nous reviendrons ultérieurement sur ce point.

initialization

cette rubrique contient une susbtitution (généralisée) qui définit la valeur initiale des variables.

operations

cette rubrique contient la définition d'une liste d'objets appelés opérations. Une opération peut modifier l'état de la machine, prendre des arguments ou (inclusif) renvoyer une valeur. Les opérations sont définies en termes de substitutions généralisées.

constants

cette rubrique contient les déclarations des noms des constantes.

constraints

cette rubrique contient les axiomes caratérisant les constantes.

L'exemple

Spécification informelle

La circulation d'un carrefour est réglée par deux feux tricolores dont les couleurs sont vert, orange ou rouge. Sur chacun des feux une seule des couleurs est active àla fois. Le système de feux du carrefour peut être en service ou hors service. Lorsque le système est hors service, les deux feux sont oranges. Lorsque le système est en service, la couleur de chacun des feux change suivant le cycle : orange puis rouge puis vert puis orange, etc ...

Un véhicule ne peut s'engager sur une voie que si le feu n'est pas rouge. Lorsque le système est en service, les feux doivent être réglés de façon àce que deux véhicules venant de voies différentes ne se trouvent pas en même temps sur le carrefour.

On désire obtenir un système assurant la mise en route du carrefour et la gestion du changement de couleur des feux.

Pré-spécification formelle

1. << les couleurs sont vert, orange ou rouge >> :
   Couleurs = {vert, orange, rouge}
2. << deux feux tricolores >> :
   feuAÎ Couleurs, feuBÎ Couleurs
3. << cycle : orange puis rouge puis vert >> :
   SuccÎ Couleurs® Couleurs
   orange|® rouge
   rouge|® vert
   vert|® orange
4. << en service ou hors service >> :
   Etats = {hs, es}
   etatÎ Etats
5. << Lorsque le système est hors service, les deux feux sont oranges >> :
   (etat = hs) Þ (feuA=orange Ù feuB=orange)
6. << Lorsque le système est en service, les feux doivent être réglés de façon àce que deux véhicules venant de voies différentes ne se trouvent pas en même temps sur le carrefour >> :
   (etat = es) Þ ((feuA=rouge Ú feuB=rouge) Ù feuA¹feuB)
   Notez que notre formule dit plus que ce que réclamait la spécification informelle. Nous avons ajoutéàla propriétéréclamée de sécurité, une propriétéde disponibilité garantissant que l'un des feux permet le passage des véhicules.

Spécification formelle

machine
 CARREFOUR

sets
 Etats = {hs, es}
 Couleurs = {vert, orange, rouge}

constants
 Succ

constraints
 SuccÎ Couleurs® Couleurs Ù
 Succ(orange)=rouge Ù
 Succ(rouge)=vert Ù
 Succ(vert)=orange

variables
 etat, feuA, feuB

invariant
 etatÎ Etats Ù
 feuAÎ Couleurs Ù
 feuBÎ Couleurs Ù

 (etat = hs) Þ (feuA=orange Ù feuB=orange) Ù
 (etat = es) Þ ((feuA=rouge Ú feuB=rouge) Ù feuA¹feuB)

initialization
 etat, feuA, feuB := hs, orange, orange

operations
 MiseEnService º
  pre  etat=hs then
   any  f₁, f₂ where
    f₁Î Couleurs Ù f₂Î Couleurs Ù
    (f₁=rouge Ú f₂=rouge) Ù f₁¹f₂
   then
    etat, feuA, feuB := es, f₁, f₂

 Changement º
  pre  etat=es then
   any  f₁, f₂ where
    f₁Î Couleurs Ù f₂Î Couleurs Ù
    (f₁=rouge Ú f₂=rouge) Ù f₁¹f₂ Ù
    (f₁= Succ(feuA))Ú (f₂= Succ(feuB))
   then
    feuA, feuB := f₁, f₂

Correction des machines abstraites

1. L'initialisation doit établir l'invariant.
2. Chaque opération doit conserver l'invariant.

machine
 M
sets
 X
variables
 x
invariant
 I
initialization
 S₀
operations
 O₁ º
  pre j  then S₁

1. [S₀]I
2. IÙj Þ [S₁]I

Correction de CARREFOUR

• I₁º etatÎ EtatsÙ feuAÎ CouleursÙ feuBÎ Couleurs
• I₂º (etat = hs) Þ (feuA=orange Ù feuB=orange)
• I₃º (etat = es) Þ ((feuA=rouge Ú feuB=rouge) Ù feuA¹feuB)

Initialisation

1. [S₀]I₁º esÎ EtatsÙ orangeÎ CouleursÙ orangeÎ Couleurs
   qui est trivialement vraie par définition des ensembles Etats et Couleurs.
2. [S₀]I₂º (hs = hs) Þ (orange=orange Ù orange=orange)
   qui est on ne peut plus trivialement vraie puisque le vrai entraîne la vrai.
3. [S₀]I₂º (es = hs) Þ ((orange=rouge Ú orange=rouge) Ù orange¹orange)
   qui est tout aussi trivialement vraie puisque le faux (es = hs) entraîne n'importe quoi.

MiseEnRoute

1. [S₁'']I₁º esÎ EtatsÙ f₁Î CouleursÙ f₂Î Couleurs.
   On a esÎ Etats par définition de l'ensemble Etats ; et f₁Î Couleurs et f₂Î Couleurs par hypothèse (y₁¹).
   
   
2. [S₁'']I₂º (es = hs) Þ (f₁=orange Ù f₂=orange)
   Ce qui est trivialement vrai puisque es ¹hs.
3. [S₁'']I₃º (es = es) Þ ((f₁=rouge Ú f₂=rouge) Ù f₁¹f₂).
   Ce qui est rendu vrai par l'hypothèse y₁².

Changement

1. [S₂'']I₁º etatÎ EtatsÙ f₁Î CouleursÙ f₂Î Couleurs.
   On a etatÎ Etats par l'hypothèse I et f₁Î Couleurs et f₂Î Couleurs par y₂¹.
2. [S₂'']I₂º (etat = hs) Þ (f₁=orange Ù f₂=orange).
   Par l'hypothèse j ₂ (la précondition), on a que etat=es. Ce qui rend trivialement vraie l'implication recherchée.
3. [S₂'']I₃º (etat = es) Þ ((f₁=rouge Ú f₂=rouge) Ù f₁¹f₂).
   Ce qui nous est donnépar I et y₂²

Commentaire sur cette première machine abstraite

Raffinement

Obligations de preuve

1. [T0]¬[S0]¬ J et
2. IÙ JÙ j ÞyÙ [T1]¬[S1]¬ J

Raffinement d'opération

Substitutions généralisées en plus

Substitution gardée

Substitution àchoix borné

Le raffinement CARREFOUR1

refinement
 CARREFOUR1

refines
 CARREFOUR

sets
 Etats = {hs, es}
 Couleurs = {vert, orange, rouge}

variables
 etat₁, feuA₁, feuB₁

invariant
 etat₁=etat Ù
 feuA₁=feuA Ù
 feuB₁=feuB

initialization
 etat₁, feuA₁, feuB₁ := hs, orange, orange

operations
 MiseEnService º
  pre  etat₁=hs then
   etat₁, feuA₁, feuB₁ := es, rouge, vert

 Changement º
  pre  etat₁=es then
   choice
    when feuA₁=vert then feuA₁ := orange
   or
    when feuA₁=orange then feuA₁,feuB₁ := rouge,vert
   or
    when feuA₁=rougeÙ feuB₁=vert then feuB₁ := orange
   or
    when feuA₁=rougeÙ feuB₁=orange then feuA₁,feuB₁ := vert,rouge

Obligations de preuves

Initialisation

Mise en service