| Enseignant | Site/Liens | Cours | TD | TP | ECTS |
|---|---|---|---|---|---|
| Cours : E. Violard TD : N. Magaud | à voir. peut être des TD/TP via racine de N. Magaud | 18 | 18 | ||
| Objectifs | |||||
| Acquérir les bases théoriques des techniques de spécification et preuve de programme. | |||||
| Contenu | |||||
| Fondements de la programmation Preuve de programmes. | |||||
| Correction partielle et terminaison. | |||||
| Préconditions, postconditions, invariants, variants. | |||||
| Logique de Hoare. | |||||
| Weakest préconditions de Dijkstra. | |||||
| Application à la construction rationnelle de programmes. | |||||
| Spécification algébrique. | |||||
| Signatures hétérogènes, variables et termes. | |||||
| Logique équationnelle, preuves déductives et inductives. | |||||
| Préconditions et équations conditionnelles. | |||||
| Eléments de sémantique dénotationelle : algèbre multisorte, évaluation, junks, confusion, initialité. | |||||
| Initiation à un langage de spécification algébrique. | |||||
| Application aux structures de données usuelles. | |||||
| Prérequis | |||||
| Logique et programmation logique, connaissance d'un langage impératif. | |||||
| Références | |||||
| BLACKHOUSER R., Program Construction and Verification, Prentice-Hall, 1986. | |||||
| BERGSTRA J.A. & al., Algebraic Specifications, Addison-Wesley, 1988. | |||||
| GOGUEN J.A. & al., Applications of Algebraic Specifications using OBJ, CUP, 1992. | |||||
| Contrôle des Connaissances | |||||
| Contrôle continu : coeff. 1/3 | |||||
| Examen écrit : coeff. 2/3 (durée : 2h) | |||||