A reuse-oriented framework for hierarchical specifications

In order to facilitate the reuse of possibly complex hierarchical specification components, we propose a unified view of them as (generalised) open terms generated by constructors : the atomic modules (for example enrichments or presentations). Thus, all kinds of pieces of specifications are handled in a uniform wagr. Moreover, they are autonomous in the sense that they are well defined independently from the context of their design. We present an equational axiomatisation of the structure, providing the class of hierarchical specifications with two combination operators. We show on the example of proofs how thanks to this approach, an attribute for a specification may be systematically inherited from the ones of its modules. The so obtained attributes are naturally structured following the specifications.