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.
Type de document :
Communication dans un congrès
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs - 2013, Feb 2013, Aussois, France. 2013
Liste complète des métadonnées


https://hal.inria.fr/hal-00778791
Contributeur : Ist Inria Saclay <>
Soumis le : lundi 21 janvier 2013 - 14:34:57
Dernière modification le : jeudi 9 février 2017 - 15:55:01
Document(s) archivé(s) le : samedi 1 avril 2017 - 07:49:45

Fichier

jfla2013-01.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00778791, version 1

Citation

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

Partager

Métriques

Consultations de
la notice

255

Téléchargements du document

213