Weakest Precondition Calculus, Revisited using Why3

Claude Marché 1, 2 Asma Tafat 1
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : Ce rapport 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 du développement de cette étude de cas, les fonctionnalités avancées de Why3 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 :
Rapport
[Research Report] RR-8185, INRIA. 2012, pp.32
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00766171
Contributeur : Claude Marché <>
Soumis le : lundi 17 décembre 2012 - 17:10:54
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : dimanche 18 décembre 2016 - 03:52:13

Fichier

RR-8185.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00766171, version 1

Collections

Citation

Claude Marché, Asma Tafat. Weakest Precondition Calculus, Revisited using Why3. [Research Report] RR-8185, INRIA. 2012, pp.32. 〈hal-00766171〉

Partager

Métriques

Consultations de la notice

333

Téléchargements de fichiers

490