====Conception Formelle====

Responsables : [[https://dept-info.labri.fr/~griffaul/| Alain Griffault]] et [[https://labri.fr/perso/vpenelle | Vincent Penelle]]

Ce cours du S8 est commun avec le parcours GL. Il vaut 6ECTS.

===Résumé===

Partie 1 (Alain Griffault) : Alta-rica (todo).

Partie 2 (Vincent Penelle) : 
[[https://www.labri.fr/perso/vpenelle/Enseignement/ConceptionFormelle/|Page de ressources]]

Cette partie du cours est consacrée à la spécification et la vérification de programmes en C grâce à la technique de calcul de Weakest Precondition, et fait pratiquer cette technique grâce au logiciel [[https://www.frama-c.com|Frama-C]].
Le cours présente les bases théorique du calcul de Weakest Precondition. Il apprend également à spécifier des contrats de fonctions en logique du premier ordre. Le logiciel Frama-C accepte de telles spécification (avec une syntaxe équivalent à la logique du premier-ordre).