Hierarchical Heterogeneous Specifications

We propose a definition of hierarchical heterogeneous formal specifications, where each module is specified according to its own homogeneous logic. We focus on the specification structure which we represent by a term in order to take benefit of classical knowledge on terms. For example, substitutions solve implementation sharing of modules. Then, we show how proof mechanisms can be expressed inside our framework. Our proof system involves both the homogeneous inference relations associated to the logics of modules and property inheritance relations associated to the structuring primitives. Heterogeneous primitives allow to move from one logic to another. We sketch out the specification of a travel agency given according to our particular framework of structured specifications. We demonstrate on this specification how a heterogeneous proof can be handled.

• Type: Conference
• Year: 1998
• Where: WADT
• Authors: Sophie Coudert, Gilles Bernot, Pascale Le Gall
• Keywords: Heterogeneous Formal Specifications, Homogeneous Inference Relations, Homogeneous Logic, Software Engineering, WADT 1998