Parameterized conditional specifications : sufficient completeness and implicit induction

Abstract : 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.
Type de document :
Rapport
[Research Report] RR-2129, INRIA. 1994
Liste complète des métadonnées

https://hal.inria.fr/inria-00074543
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 15:43:44
Dernière modification le : samedi 17 septembre 2016 - 01:06:53
Document(s) archivé(s) le : mardi 12 avril 2011 - 17:26:37

Fichiers

Identifiants

  • HAL Id : inria-00074543, version 1

Collections

Citation

Adel Bouhoula. Parameterized conditional specifications : sufficient completeness and implicit induction. [Research Report] RR-2129, INRIA. 1994. 〈inria-00074543〉

Partager

Métriques

Consultations de la notice

84

Téléchargements de fichiers

37