Calcul de plus faible précondition, revisité en Why3

Claude Marché 1, 2 Asma Tafat 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Cet article a deux objectifs. D'une part, nous présentons une méthode originale de preuve de correction d'un calcul de plus faible précondition, fondée sur la notion de sémantique bloquante. La méthode imite au niveau des spécifications logiques la méthode classique de preuve de type soundness. D'autre part, cette preuve est réalisée formellement dans l'environnement de vérification déductive Why3, et nous illustrons, au fur et à mesure de l'article, les fonctionnalités avancées de cet environnement que nous avons utilisées. Le résultat constitue une présentation revisitée du calcul de plus faible précondition, et qui, bien qu'elle soit réalisée formellement, est facile à suivre, grâce en particulier au haut degré d'automatisation des preuves qui permet de se focaliser sur les points clés.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-00778791
Contributor : Ist Inria Saclay <>
Submitted on : Monday, January 21, 2013 - 2:34:57 PM
Last modification on : Thursday, April 5, 2018 - 12:30:22 PM
Long-term archiving on : Saturday, April 1, 2017 - 7:49:45 AM

File

jfla2013-01.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-00778791, version 1

Collections

Citation

Claude Marché, Asma Tafat. Calcul de plus faible précondition, revisité en Why3. JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France. ⟨hal-00778791⟩

Share

Metrics

Record views

365

Files downloads

317