Séance
2
1) FAIRE le TP ECLUSE
===============
2) FAIRE le TP RESERVATION
===================
1) Charger les fichiers :
- RESERVATION.mch : la spécification
- RESERVATION1.ref : le raffinement
- CODE.imp : une implémentation
- USER1.mch et USER1_i.imp : une utilisation du service
réservation
Les fichiers
2) Raffinement RESERVATION1 : on représente l'ensemble occupes
par un tableau de
booléens appelé etat (TRUE si dans occupés, FALSE
sinon).
Compléter l'invariant et l'initialisation et faire les preuves.
3) Implémentation CODE : compléter l'invariant et le
variant de la boucle de l'opération
réserver et faire les preuves.
4) Générer le code à partir de USER_I et
exécuter