Note : vous pouvez travailler sur l'ancienne version de ce bureau d'étude, qui utilise les outils krakatoa et why pour faire des preuves similaires sur des programmes Java. L'ancienne version vous permet de travailler de manière plus autonome, la nouvelle vous permet d'approfondir les concepts liés à la définition d'une sémantique axiomatique.

Télécharger l'archive suivante: Sem2015_BE.zip, et compléter la définition de la sémantique axiomatique de Niklaus (fichier NikAxiomatic.thy). Pour simplifier votre tâche, les instructions d'entrée/sortie de Niklaus (Read et Write) ont été supprimées de cette version.

Compléter ensuite les théories PGCD.thy et NikPGCD.thy pour prouver que l'implémentation en Niklaus de l'algorithme d'Euclide (par soustractions successives) calcule bien le PGCD de deux entiers.

Déposer l'archive ZIP de votre travail sur http://wwwdi.supelec.fr/Livraison.