zbMATH — the first resource for mathematics

Abstract and behaviour module specifications. (English) Zbl 0923.68089
Summary: The theory of algebraic module specifications and modular systems was developed initially mainly on the basis of equational algebraic specifications. We show that it is in fact almost independent of what kind of underlying specification framework is chosen. More specifically, we present a formulation where this framework appears as an indexed category or, equivalently, specification frame. The ensuing theory is called the theory of abstract module specifications. We are able to prove main results concerning the correctness and compositionality of abstract module specifications in a purely categorical way, assuming the existence of pushouts of morphisms between abstract specifications that allow model amalgamation, functor extension and/or suitable free constructions. Then, by instantiating the theory of abstract module specifications to the behaviour specification frame in the sense of Nivela and Orejas. we obtain a theory of behaviour module specifications.

68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
18C50 Categorical semantics of formal languages
Full Text: DOI