TY - JOUR
T1 - Composing hidden information modules over inclusive institutions
AU - Goguen, Joseph
AU - Roşu, Grigore
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=26944448737&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=26944448737&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-39993-3_7
DO - 10.1007/978-3-540-39993-3_7
M3 - Article
AN - SCOPUS:26944448737
SN - 0302-9743
VL - 2635
SP - 96
EP - 123
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -