# Observational Proofs by Implicit Context Induction

Observational Proofs by Implicit Context Induction - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.

Keywords : observability context induction implicit induction conditional specification

Autor: Narjes Berregeb - Adel Bouhoula - Michaël Rusinowitch -

Fuente: https://hal.archives-ouvertes.fr/

DESCARGAR PDF