Cours : Introduction à la sémantique
Responsable : Yves Bertot
Objectifs :
- Décrire la partie "comportement" des langages de programmation,
- Raisonner de façon systématique sur les programmes,
- Prouver la correction de transformations de programmes.
Structure :
- 9 heures de cours
- 12 h de TD ou TP
Évaluation :
Programme :
- Un petit langage impératif et sa sémantique naturelle,
- Un petit langage fonctionnel et sa sémantique naturelle,
- Démonstrations par récurrence sur les programmes et sur la sémantique,
- Programmes annotés et calcul de la précondition la plus faible,
- Techniques de preuves de programmes avec boucles: recherches d'invariant
- Utilisation d'un outil de preuve de programmes: Frama-C (ou Caduceus).
Pré-requis :
Références :