Calcul de plus faible précondition, revisité en Why3
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.
Origine : Accord explicite pour ce dépôt
Loading...