Skip to Main content Skip to Navigation

Generalizing CASL Specification Components and Preserving Rewrite Proofs

Anamaria Martins Christophe Ringeissen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose the theoretical basis of a tool for the generation of reusable CASL specification components by generalization of existing ones. The underlying idea is, given a component and a set of semantic properties that it satisfies and that we want to preserve, to find a parameterized, more general, component satisfying the following conditions: the original component is one of its possible instantiations, and any of its instantiations satisfy the stated properties. We present here both the definition of the generalization operation for CASL and the problem of preserving properties in the generalized component. To guarantee the preservation of properties, we propose to preserve their proofs, concentrating on the use of rewrite proofs. This technique provides a simple way to find sufficient conditions for the preservation of the corresponding properties. This work is being integrated in the specification component development tool FERUS, under development for the CASL language, using ELAN as the rewrite proof engine.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:23:01 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:30:40 PM


  • HAL Id : inria-00071641, version 1



Anamaria Martins, Christophe Ringeissen. Generalizing CASL Specification Components and Preserving Rewrite Proofs. [Research Report] RR-4938, INRIA. 2003, pp.34. ⟨inria-00071641⟩



Record views


Files downloads