SEANCE
1
ON NE FERA QUE DES PREUVES AUTOMATIQUES EN
FORCE 0 OU 1
Pour les exercices suivants normalement il reste peu (voire pas) de
preuves interactives.
En tous les cas au-dessus de 5 c'est qu'il y a un problème dans
les invariants.
Pour les preuves interactives restantes :
- essayer pp.0 et pp.1
- les regarder pour vérifier si elles sont
démontrables. Ecrire le scénario de preuve sur une
feuille. On pourra ensuite
les faire à l'aide du prouveur interactif.
2) FAIRE le TP DIVISION
===============
Charger les fichiers : les
fichiers
- DIV.mch : la spécification
- DIV_I.imp : l'implémentation à compléter
- MachineDeTest.mch et MachineDeTest_imp.imp : pour tester la
division
1- Compléter DIV_I.imp et faire les preuves
2 - générer le code et tester la division
Pour cela charger les fichiers suivants dans le répertoire
lang/c
( basic_io.h ,
basic_io.c
et main.c)
3) FAIRE LE TP RECHERCHE
==================
Charger les fichiers : les
fichiers
- recherche.mch : la spécification
- recherche2.imp : le programme à compléter
Le fichier recherche2.imp contient une opération IndiceVal dont
le comportement est décrit dans le fichier
recherche.mch.
Nous voulons décrire le corps de cette opération. Pour
cela nous utilisons une boucle et
3 variables locales : trouve, IndexCour et tmp.
Complétez cette opération et vérifiez la
correction de votre
proposition par la preuve. Si certaines obligations de preuves ne
peuvent etre résolues automatiquement,
alors expliquez de manière détaillée
comment les prouver.