Le plan du cours change d'année en année. Vous pouvez accéder au cours tel que je l'avais fait (ou avais prévu de le faire) en 2000-2001, 2001-2002, 2002-2003, 2003-2004, 2004-2005, 2007-2008.
Dans la première partie du cours, nous apprendrons à nous servir d'un système de démonstration sur ordinateur. Nous utiliserons ensuite ce système de démonstration sur ordinateur pour décrire précisément un petit langage de programmation, pour développer des outils manipulant des programmes de ce langage de programmation, et pour montrer que ces outils sont corrects, au sens où il permettent d'éviter l'introduction d'erreurs de programmation ou de détecter certaines classes d'erreurs.
Les notes pour le premier cours sont disponibles ici .
La première séance de travaux dirigés repose sur le document suivant. Un exemple supplémentaire est fourni dans cet exercice sur la somme de carrés
écrivez la fonction sop5 qui additionne les premieres puissances cinquièmes:
1 + 32 + 243 + ... +n^5
Trouvez une formule de la forme : forall x, k*sop5 x = l*x^6 + .... puis démontrez que cette formule est correcte. Tout doit être fait dans Coq. (inspirez-vous de l'exemple sos).
Dans cette partie du cours nous montrons comment décrire les structures syntaxiques d'un petit langage de programmation. Ensuite nous montrons comment décrire le comportement des instructions de ce langage. Nous concluons en montrant comment tout ce travail peut être implémenté dans Coq. Le cours est principalement basé sur ces notes de cours.
En vous inspirant du code dans les fichiers syntax.v, td2.v et boxes.v écrivez une fonction de type instr -> string qui affiche une instruction de façon lisible.
Dans cette partie du cours, nous montrons comment on peut démontrer que les variables des programmes satisfont certaines propriétés. Ce cours introduit les notions de pré-condition post-condition et d'invariant de boucle. Les notes de ce cours sont disponibles ici.
On fera le travail décrit dans ce fichier.
Dans cette partie du cours, nous étudions une méthode de vérification des programmes qui consistent à annoter ces derniers avec des propriétés logiques. Deux fonctions peuvent être définies pour calculer la condition la plus faible pour que le programme soit appelé dans les conditions prévues par les annotations et les conditions logiques pour que le programme soit cohérent avec ses annotations. Dans le cours, on démontre que ces fonctions sont correctes, au sens ou leur comportement est équivalent à la construction d'une dérivation de logique de Hoare.
On fera le travail décrit dans ce fichier.
Ecrivez dans le langage de programmation impératif étudié en cours un programme qui calcule la racine carrée de l'une de ses entrées, lorsque cette entrée est positive. Annotez le programme pour exprimer cette spécification et démontrez que le programme satisfait la spécification en utilisant le théorème vcg_correct du quatrième TD.
Pas de cours pour cette semaine. Nous allons reprendre des preuves autour de la sémantique naturelle (comme en deuxième semaine). Le sujet du TD est disponible ici.