L'objectif est simple : on pose des contrat pre et post sur un morceaux de code, on peut aussi poser des invariants au sein d'une boucle, et le logiciel ( http://why.lri.fr/index.fr.html ) qui est tiré de cette thèse :
- Prouve la complétude et l'adéquation des contrats au code
- Prouve que le code respecte les contrats
Plus fort que (…)