Les bugs c’est mal. Exemples et anecdotes (rapide).
On veut les éviter. Validation VS Vérification.
Première question importante : qu’est-ce qu’un bug ?
Vérification
Vérification partielle
Modules principaux:
Dans ce cours, on se concentre sur les deux derniers modules.
ACSL - Ansi-C Specification Language.
Syntaxe basique: se note comme un commentaire spécial du C : /*@ ... */.
Concept crucial: Contrat de fonction. Décrit la spécification d’une fonction avant sa déclaration.
Autres concepts qu’on verra plus tard:
Weakest Precondition (Dijkstra):
Ajouter quelque chose pour les appels de fonctions ? (sans effets de bords dans ce cas)
petit exo.
Ça aussi c’est dur à automatiser (il faut trouver la quantité). Voire on ne connait pas le résultat (ex: suite de Syracuse).
Todo: exo. Division euclidienne (cf ci-dessus), PGCD, racine carrée, recherche dichotomique.
recherche dichotomique:
Règle générale. {P} while(t) e; {Q} | {I && t && val\in D && val == α} e {I && val\in D && val REL α} /\ I && ¬t ==> Q /\ P ==> I /\ REL est un ordre bien fondé sur D.