Proofs in parameterized specifications

Abstract : Theorem proving in parameterized specifications has strong connections with inductive theorem proving. An equational theorem holds in the generic theory of the parameterized specification if and only if it holds in the so-called generic algebra. Provided persistency, for any specification morphism, the translated equality holds in the initial algebra of the instantiated specification. Using a notion of generic ground reducibility, a persistency proof can be reduced to a proof of a protected enrichment. Effective tools for these proofs are studied in this paper.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00075136
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 5:31:48 PM
Last modification on : Saturday, September 17, 2016 - 1:06:49 AM
Long-term archiving on : Tuesday, April 12, 2011 - 9:22:16 PM

Identifiers

  • HAL Id : inria-00075136, version 1

Collections

Citation

Hélène Kirchner, Claude Kirchner. Proofs in parameterized specifications. [Research Report] RR-1424, INRIA. 1991. ⟨inria-00075136⟩

Share

Metrics

Record views

155

Files downloads

171