U NIVERSITÉ DE T UNIS E L M ANAR 2020-2021
FACULTÉ DES S CIENCES DE T UNIS
————
D ÉPARTEMENT DES S CIENCES DE
L’I NFORMATIQUE
A PPROCHES F ORMELLES DE D ÉVELOPPEMENT DES L OGICIELS
C ORRECTION T.D.N O 1
Méthode B abstract machine notation (AMN)
Section : IF5
Enseignantes : Yousra Hlaoui & Salma Ayari
Rappel Du cours :
Clauses d’une machine abstraite
— MACHINE ( ) NomMachine(liste de paramètres)
— CONSTRAINTS Propriétés ds paramètres
— SETS Liste des ensembles abstraits et enumérés
— CONSTANTS Liste des constantes
— PROPERTIES Propriétés des constantes et ensembles
— VARIABLES Liste des variables d’état
— INVARIANT Typage et propriétés des variables
— DEFINITIONS Liste des définitions
— INITIALISATION Initialisation des variables
— OPERATIONS Liste des opérations
Exercice 1
1. MACHINE Students
SETS Student
CONSTANTS max_students /* pour borner le sous-ensemble de travail */
PROPERTIES max_students : NAT1 & max_students <100
VARIABLES studentset
INVARIANT studentset <: Student & card(studentset)<= max_students
1
INITIALISATION studentset := {}
OPERATIONS
enter(st) = /* ajoute un etudiant st a l’ensemble*/
PRE
st : Student & st /: studentset & card(studentset)< max_students
THEN studentset := studentset ∪ {st}
END;
remove(st) = /* enleve l’etudiant st de l’ensemble */
Pre
st : Student & st : studentset
THEN
studentset := studentset - {st}
END
END
2. Preuves : [Init]Invariant ⇒ Pour la clause initialisation : On prouve que l’initialisation
vérifie l’invariant. [init]I => [studentset := {} ]studentset< : Student & card(studentset)<=
max_student ⇒ {} < : Student & card({})<= max_student ⇒ vrai
I ∧ Q ⇒ [V ]I ⇒ lorsque lópération est appelée avec la pré-condition Q. Láppel est
supposée vérifiée alors sa transformation V amène la machine dans un état correct un
état qui satisfait línvariant I.
Studentset <: student ⇒ studentset∪{st} <: studentset <: Student&card(studentset) <=
max_student&st ∈ student&st ∈ / studentset&card(studentset) < max_students ⇒
[studentset∩{st}]studentset <: Student&card(studentset) <= max_studentstudentset ⊆
Student&st ∈ / studentset&card(studentset) < max_students ⇒ studentset ∩ {st} ⊆
Studentquiestvaluvraicarstudentset ⊆ Student&st ⊆ Student(Hypothse)quiimpliqueque
studentset ∩ {st} ⊆ Student&card(studentset + 1) <= max_students.
Exercice 2
T rainarrive/N := 1
start levee baissee T rainarrive/N := N + 1,
N := 0 T rainpart[N > 1]/N := N − 1
T rainpart[N = 1]/N := 0
1.
2
2. En B, les états de áutomate constituent un ensemble abstrait et chaque transition est
une opération.
MACHINE
BARRIERE
SETS
ETATS = levee,baisse
VARIABLES
etat , number
INVARIANT
number : NAT &
etat : ETATS &
((etat = levee)=>number =0)
INITIALISATION
number := 0 || etat := levee
OPERATIONS
trainarrive=
PRE
etat=levee & number = 0
THEN
number := number +1 || etat := baisse
END ;
trainpart =
PRE
etat = baisse & number >=1
THEN
IF(number>1) THEN
etat := baisse || number := number-1
ELSE
etat := levee || number :=0
END
END
END
