Pré-requis [SuitableStuff]

Pré-requis

Critères de qualité d'un système logiciel et enjeux de la certification. Exemples avec les langages et ateliers VDM, Z, B, UML…
Certification assistée par ordinateur avec Coq.
- Compléments sur le langage, les tactiques et les librairies.
- Techniques de définition de types et stratégies de preuves.
- Pré et post-conditions, invariants, gestion des exceptions.
- Modules et généricité des descriptions. Traduction en Coq des spécifications écrites dans d'autres systèmes.
Construction et certification de bibliothèques de programmes.
- Formulation du raffinement de représentations de données.
- Obligations de preuves.
- Certification de la correction d'une implantation.
- Passage à la programmation concrète dans les différents types de langages.

Connaître les différentes techniques de spécification, preuve et vérification de logiciel
Spécifier de manière formelle les parties critiques des logiciels
Découvrir et énoncer les propriétés qu'elles doivent vérifier
Mettre en oeuvre un système d'assistance à la spécification et à la preuve
Maîtriser le processus de raffinement de spécifications jusqu'à l'obtention d'un programme correct

J.-F. Monin, Undestanding Formal Methods, Springer, 2003
Y. Bertot and P. Casteran, Theorem Proving and Program Development - Coq'Art, Texts in TCS, An EATCS Series, Springer-Verlag, 2004
J.-R. Abrial, The B_Book - Assigning Programs to Meanings, Cambridge Univ. Press, 1996
J.-Y. Girard et al., Proofs and Types, In Cambridge Tracts in TCS, Cambridge Univ. Press, 1989
E. Gamma et al., Design Patterns, Thomson Publishing, 1996