Proofs by implicit induction : case of associative-commutative and observational theories
Preuves par induction implicite : cas des théories associatives-commutatives et observationnelles
Résumé
Automated induction proofs are a formal means for systems validation. In the framework of test set induction, we propose two automated proofs methods for conditional specifications: one deals with associative-commutative (AC) theories, the other with observational theories. In the first method, we give an algorithm for computing induction schemes, as well as a new inference system using elaborated AC rewriting techniques. For a class of specifications, the method detects non valid conjectures in a finite time. Interesting experiments on the correctness of digital circuits produced proofs requiring less interaction than other well-known provers. In the observational approach, data type objects are cnsidered as equal if they cannot be distinguished by experiments with observational results. These experiments are represented by particular terms called observable contexts. We propose an automated proof method of observational properties, relying on the computation of a finite set of well-chosen contexts called test contexts, that shematizes all the observable contexts. We also propose methods for computing such test contexts and a new inference system. For an interesting class of specifications, the method detects non observationally valid conjectures in a finite time.
Les preuves automatiques par induction sont un moyen formel pour la validation de systèmes informatiques. Dans le cadre de l'induction par ensemble test, nous proposons deux méthodes de preuves automatiques s'appliquant à des spécifications conditionnelles : l'une opérant dans les théories associatives-commutatives (AC), l'autre dans les théories observationnelles. Dans la première méthode nous proposons un calcul des schémas d'induction, ainsi qu'un système d'inférence utilisant des techniques élaborées de réécriture modulo AC. Pour une classe de spécifications, la méthode détecte toute conjecture non valide en un temps fini. Des expérimentations intéressantes sur la correction de circuits digitaux, ont produit des preuves nécessitant moins d'interaction qu'avec d'autres prouveurs connus. Dans l'approche observationnelle, les objets d'un type de données sont considérés comme égaux s'ils ne peuvent être distingués par des expérimentations à résultats observables. Ces expérimentations sont représentées par des termes particuliers appelés contextes observables. Nous proposons une méthode de preuve automatique de propriétés observationnelles reposant sur le calcul d'un ensemble fini de contextes, appelés contextes tests, qui schématise l'ensemble de tous les contextes observables. Nous proposons également des méthodes de calcul de ces contextes tests ainsi qu'un nouveau système d'inférence. Pour une classe de spécifications, la méthode détecte toute conjecture non observationnellement valide en un temps fini.