Observational proofs by rewriting - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 2002

Observational proofs by rewriting

Résumé

Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker (Hennicker, Formal Aspects of Computing 3(4) (1991) 326–345). We propose in this paper to embed Context Induction in the implicit induction framework of (Bouhoula and Rusinowitch, Journal of Automated Reasoning 14(2) (1995) 189–235). The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.

Domaines

Autre [cs.OH]

Dates et versions

inria-00100714 , version 1 (26-09-2006)

Identifiants

Citer

Adel Bouhoula, Michaël Rusinowitch. Observational proofs by rewriting. Theoretical Computer Science, 2002, 275 (1-2), pp.675-698. ⟨10.1016/S0304-3975(01)00333-4⟩. ⟨inria-00100714⟩
59 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More