On the Algebra of the Structured Specifications(abstract)
We develop module algebra for structured specifications with model
oriented denotations. Our work ex tends the existing theory with
specification building operators for non-protecting importation modes
and with new algebraic rules (most notably for initial semantics) and
upgrades the pushout-style semantics of parameterized modules to
capture the (possible) sharing between the body of the parameterized
modules and the instances of the parameters. We specify a set of
sufficient abstract conditions, smoothly satisfied in the actual
situations, and prove the isomorphism between the parallel and the
serial instantiation of multiple parameters. Our module algebra
development is done at the level of abstract institutions, which means
that our results are very general and directly applicable to a wide
variety of specification and programming formalisms that are
rigorously based upon some logical system.
back to Selected Publications