II2-ENSI-GL2
1
Exemple : Réservation de places
sur un vol limité à maxi places
MACHINE
RESERVATION1
CONSTANT
Maxi
PROPERTIES
Maxi NAT
Advertisement
VARIABLES
Nb
INVARIANT
INITIALISATION
Nb := Maxi
Nb 0..Maxi /nbre de places/
OPERATIONS
Réserver=
PRE Nb 0
THEN
Advertisement
Nb := Nb –1
END ;
Libérer=
PRE Nb Maxi
THEN
Nb := Nb + 1
END
END
II2-ENSI-GL2
2
Advertisement
Exemple : Réservation de places sur
un vol limité à maxi places
Calcul des obligations de preuve :
Pour l’initialisation :
Maxi NAT [Init]I =
Maxi NAT [Nb := Maxi](Nb 0..Maxi)
= Maxi NAT Maxi 0..Maxi = True
L’outil effectue la preuve et prouve que
[Init]I est un théorème
Pour l’opération Réserver :
Advertisement
Maxi NAT (Nb 0..Maxi) Nb 0 [Nb := Nb –1] (Nb 0..Maxi)
= Maxi NAT (Nb 1..Maxi) (Nb-1 0..Maxi)
= True
Pour l’opération libérer :
Maxi NAT (Nb 0..Maxi) Nb Maxi [Nb := Nb +1] (Nb 0..Maxi)
= Maxi NAT (Nb 0..Maxi-1) (Nb+1 0..Maxi)
= True