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.
Type de document :
Rapport
[Research Report] RR-1424, INRIA. 1991
Liste complète des métadonnées

https://hal.inria.fr/inria-00075136
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 17:31:48
Dernière modification le : samedi 17 septembre 2016 - 01:06:49
Document(s) archivé(s) le : mardi 12 avril 2011 - 21:22:16

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

138

Téléchargements de fichiers

94