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 :

2) FAIRE le TP DIVISION
===============


Charger les fichiers : les fichiers


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


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.