Parameterized conditional specifications : sufficient completeness and implicit induction - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1994

Parameterized conditional specifications : sufficient completeness and implicit induction

Adel Bouhoula
  • Fonction : Auteur
  • PersonId : 756484
  • IdRef : 132449021

Résumé

Theorem proving in parameterized specifications allows for shorter and more structured proofs. Moreover, a generic proof can be given just once and reused for each instantiation of the parameters. We present procedures to test sufficient completeness and to prove and disprove inductive properties automatically in parameterized conditional specifications. Our method relies on the notion of test set, which can be seen as a well-suited induction scheme. Previously, we could only compute a test set for conditional specifications if the constructors were free. Here, we give a new definition of test sets and an algorithm to compute them even if the constructors are not free. The method uses a new notion of provable inconsistency which allows us to refute more false conjrectures than with previous approaches. This new method when limited to non parameterized conditional specifications, can refute general clauses, refutational completeness is also preserved for boolean ground convergent rewrite systems with completely defined functions even if the constructors are not free. The method has been implemented in the prover SPIKE. Based on computer experiments, the method appears to be more practical and efficient than inductive theorem proving in non-parameterized specifications.
Fichier principal
Vignette du fichier
RR-2129.pdf (1.65 Mo) Télécharger le fichier

Dates et versions

inria-00074543 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00074543 , version 1

Citer

Adel Bouhoula. Parameterized conditional specifications : sufficient completeness and implicit induction. [Research Report] RR-2129, INRIA. 1994. ⟨inria-00074543⟩
43 Consultations
16 Téléchargements

Partager

Gmail Facebook X LinkedIn More