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, 2005-2006, 2006-2007, 2007-2008, 2008-2009.
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 .
Tout est dans le fichier suivant: sem2010td1.v
Voici la solution : sem2010td1sol.v
é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).
Quelques liens utiles:
Tout est dans le fichier suivant: sem2010td2.v
Voici la solution.
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.
C'est dans ce fichier.
Voici la solution.
Cette semaine nous nous concentrerons sur les preuves par récurrence sur les dérivations et les étapes de preuve par inversion.
La propriété à laquelle nous nous intéressons est l'inverse de la propriété que nous avons vue au td de la quatrième semaine. C'est dans sem2010td5.v.
Voici la solution.
C'est dans sem2010dm5.v. C'est un devoir qui fait appel au preuves par récurrences sur les dérivations (en Coq, preuves par récurrence sur les propriétés inductives).
Cette semaine, nous étudierons les fonctions qui permettent de simuler l'exécution d'un programme
Ce TD est une implémentation directe du cours, il s'agit de montrer que la fonction définie en cours est correcte. Voici le fichier
Voici la solution.