Observational Proofs by Implicit Context Induction

Narjes Berregeb 1 Adel Bouhoula 1 Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the powerful concept of {\em Context Induction} has been developed by Hennicker \citeHen. We propose in this paper to embed Context Induction in the implicit induction framework of \cite{BouhoulaR- -JAR95}. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false conjectures. Under reasonable assumptions it is refutationally complete. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.
Type de document :
Rapport
[Research Report] RR-3151, INRIA. 1997, pp.35
Liste complète des métadonnées

https://hal.inria.fr/inria-00073538
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:09:10
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:49:32

Fichiers

Identifiants

  • HAL Id : inria-00073538, version 1

Collections

Citation

Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch. Observational Proofs by Implicit Context Induction. [Research Report] RR-3151, INRIA. 1997, pp.35. 〈inria-00073538〉

Partager

Métriques

Consultations de la notice

127

Téléchargements de fichiers

100