Ci-dessous, les différences entre deux révisions de la page.
| if-cf [2020/10/07 13:59] – créée vpenelle | if-cf [2020/10/07 13:59] (Version actuelle) – vpenelle | ||
|---|---|---|---|
| Ligne 12: | Ligne 12: | ||
| [[https:// | [[https:// | ||
| - | 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, | + | 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, |
| 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). | 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). | ||