Spécification et Validation de Programmes
SVP

MANIFESTE

Partie 1

Cette première partie du cours s’articule en 3 thèmes
- Programmation récursive, définitions inductives et récurrence structurelle
- Un premier exemple de spécification et de preuve de programme
- Un exemple plus poussé de spécification et preuve d’une fonction de tri

Notes de cours

Scripts Coq (renommer les .bin en .v) :
- récurrence structurelle
- préfixe
- tri par arbre

Sujets de travaux sur machine

- Récurrence structurelle sur les entiers TME1
- Récurrence structurelle sur les listes TME2
- Listes triéesTME3/4

Partie 2

Partie 3

 
Documents utiles