Composing hidden information modules over inclusive institutions

Abstract

This paper studies the composition of modules that can hide information, over a very general class of logical systems called inclusive institutions. Two semantics are given for the composition of such modules using five familiar operations, and a property called conservativity is shown necessary and sufficient for these semantics to agree. The first semantics extracts the visible properties of the result of composing both the visible and hidden parts of modules, while the second uses only the visible properties of the components; the two semantics agree when the visible consequences of hidden information are enough to determine the result of the composition. A number of "laws of software composition" are proved relating the five composition operations. Inclusive institutions simplify many of the proofs. The approach has application to module composition technology, for both programs and specifications. © Springer-Verlag Berlin Heidelberg 2004.