Preuve de programmes en logique de Hoare

Projet pour le cours [PLOG] 2011.

1. Présentation

   La logique de Hoare (1969) est une forme systématique et automatisable de la méthode de preuve de programmes impératifs par assertions due à Floyd (1967).
   Le but du projet est d'en donner une réalisation en Prolog.
   
   On se limite ici au cas le plus élémentaire de programmes écrits dans le "micro-langage" MIL
   opérant sur des entiers, avec comme constructions
   
   • les expressions arithmétiques avec quatre opérateurs +, *, - , /  (division entière) ;
   • les comparaisons d'expressions arithmétiques (à valeur booléenne)
   • l'affectation
   • la séquence
   • la conditionnelle bilatère
   • la boucle while, munie de son invariant.
     
     
   Ces programmes sont donnés en syntaxe abstraite sous forme de documents XML.
   En voici quelques exemples.
   (Au sujet de leur représentation comme des termes Prolog, voyez mil_H.pl et tradXML_H.pl,
   variantes de programmes présentés en cours.)
   
   La validité du programme se détermine par rapport à
   
   • une précondition, supposée être vérifiée avant l'exécution,
   • une postcondition, qui doit être vérifiée à la fin de l'exécution, si le programme se termine
     (on ne cherche pas à prouver la terminaison).
     
     
   Notez que la précondition, la postcondition et les invariants de boucle sont a priori des formules quelconques.
   Nous n'utiliserons que des formules propositionnelles où les atomes sont
   
   • des expressions booléennes du langage
   • des prédicats supplémentaires, comme par exemple
Q(x,y) signifiant "y divise x et le quotient x/y est une puissance de 2".
     
   
   Exemple.
   
   La logique de Hoare a pour fonction d'exhiber les conditions de vérification,
   c'est-à-dire les propriétés qui doivent être vraies pour que la précondition implique effectivement la postcondition
   à travers l'exécution du programme.
   En voici une réalisation en Prolog, explication, programme.
   
   Suite de l'exemple.
   
   Démontrer que ces conditions sont effectivement vérifiées est une autre histoire...
   La validité du programme peut parfaitement reposer sur des propriétés arithmétiques fines qui restent hors de portée de la démonstration automatique !
   
   Le projet a pour but de construire un programme Prolog démontrant le plus possible de conditions de vérification dans la collection précitée (voici la signification des prédicats supplémentaires).
   
   

2. Premiers pas
   

   Je vous propose d'utiliser pour chaque condition de vérification le programme Wang (théorie, fichier Wang.pl),
   qui démonte la structure logique pour la réduire à sa forme normale conjonctive.
   Je vous rappelle que la représentation d'une clause en Prolog par un couple de listes comme "[[x, y, z], [u, v]]"
   s'interprète comme une implication "(x⋀y⋀z) ⊃ (u⋁v)".
   En l'occurrence les atomes ne sont plus des variables propositionnelles mais des comparaisons arithmétiques
   (ou des applications de prédicats supplémentaires).
   
   Mais cette technique s'applique mieux à des conditions de vérification normalisées pour en extraire toute la logique,
   par exemple en remplaçant "b<=a" par "0<a-b ou 0=a-b".
   
   Les prédicats définis dans norm.pl permettent de régler des cas très faciles (exemple1, exemple2), il s'agit d'aller plus loin !
   
   Très vite se pose le problème de la stratégie de preuve.
   On distingue en effet deux parties bien distinctes,
   
   • l'une visant les règles du calcul arithmétique (associativité, commutativité, distributivité, etc),
     
   • l'autre les conséquences logiques des informations connues du système (notamment sur le rôle de l'égalité).
     
   
   L'idée est d'utiliser systématiquement le programme Wang pour traiter les aspects logiques.
   Encore faut-il le mettre en œuvre à bon escient.
   
   La statégie du prédicat voirCV détini dans le fichier norm.pl est
   
   1. d'effectuer d'abord une normalisation/simplification arithmétique (prédicat normTop),
      
   2. puis d'appliquer Wang,
      
   3. et enfin d'éliminer les énoncés qui sont "évidemment vrais" vu les connaissances du système
      (prédicat spll).
   
   On a le choix (non exclusif !) entre :
   
   • garder cette stratégie et perfectionner la normalisation/simplification arithmétique ;
     
   • envisager un nouvel appel à Wang avec des connaissances étendues.
     
   
   Vous aurez d'autres idées !
   À suivre...