Observational Proofs by Implicit Context Induction - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1997

Observational Proofs by Implicit Context Induction

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-3151.pdf (401.83 Ko) Télécharger le fichier

Dates et versions

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

Identifiants

  • HAL Id : inria-00073538 , version 1

Citer

Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch. Observational Proofs by Implicit Context Induction. [Research Report] RR-3151, INRIA. 1997, pp.35. ⟨inria-00073538⟩
65 Consultations
74 Téléchargements

Partager

Gmail Facebook X LinkedIn More