In order to facilitate the reuse of possibly complex hierar-chical 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 way. 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.
Keywords formal structured specification - reuse - proof system - structured inference - typed equational logic - monoid - language theory
This work was partly supported by the ESPRIT-IV Working Group 22704 ASPIRE and by the ESPRIT-IV Working Group 23531 FIREworks