Abstract
Compositional designs require component specifications that can be composed: Designers have to be able to deduce system properties from components specifications. On the other hand, components specifications should be abstract enough to allow component reuse and to hide substantial parts of correctness proofs in components verifications. Part of the problem is that too abstract specifications do not contain enough information to be composed. Therefore, the right balance between abstraction and composability must be found. This paper explores the systematic construction of abstract specifications that can be composed through specific forms of composition called existential and universal.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)
Abadi, M., Merz, S.: An abstract account of composition. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 499–508. Springer, Heidelberg (1995)
Mani Chandy, K., Sanders, B.: Reasoning about program composition (submitted for publication), http://www.cise.ufl.edu/~sanders/pubs/composition.ps
Charpentier, M.: Assistance à Répartition de Systèmes Réactifs. Thèse de doctorat, Institut National Polytechnique de Toulouse (November 1997)
Charpentier, M., Mani Chandy, K.: Examples of program composition illustrating the use of universal properties. In: Rolim, J.D.P. (ed.) IPPS-WS 1999 and SPDP-WS 1999. LNCS, vol. 1586, pp. 1215–1227. Springer, Heidelberg (1999)
Charpentier, M., Chandy, K.M.: Towards a compositional approach to the design and verification of distributed systems. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 570–589. Springer, Heidelberg (1999)
Collette, P.: Composition of assumption-commitment specifications in a Unity style. Science of Computer Programming 23, 107–125 (1994)
Collette, P.: Design of Compositional Proof Systems Based on Assumption- Commitment Specifications. Application to Unity. Doctoral thesis, Faculté des Sciences Appliquées, Université Catholique de Louvain (June 1994)
Collette, P., Knapp, E.: Logical foundations for compositional verification and development of concurrent programs in Unity. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 353–367. Springer, Heidelberg (1995)
Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Texts and monographs in computer science. Springer, Heidelberg (1990)
Fiadeiro, J.L., Maibaum, T.: Verifying for reuse: foundations of object-oriented system verification. In: Makie, I., Hankin, C., Nagarajan, R. (eds.) Theory and Formal Methods, pp. 235–257. World Scientific Publishing Company, Singapore (1995)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Misra, J.: A logic for concurrent programming: Safety. Journal of Computer and Software Engineering 3(2), 239–272 (1995)
Sanders, B.A.: Eliminating the substitution axiom from Unity logic. Formal Aspects of Computing 3(2), 189–205 (1991)
Sivilotti, P.A.G.: A Method for the Specification, Composition, and Testing of Distributed Object Systems. PhD thesis, California Institute of Technology, 256-80 Caltech, Pasadena, California 91125 (December 1997)
Udink, R.T.: Program Refinement in Unity-like Environments. PhD thesis, Utrecht University (September 1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Charpentier, M., Chandy, K.M. (2000). Theorems about Composition. In: Backhouse, R., Oliveira, J.N. (eds) Mathematics of Program Construction. MPC 2000. Lecture Notes in Computer Science, vol 1837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722010_12
Download citation
DOI: https://doi.org/10.1007/10722010_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67727-7
Online ISBN: 978-3-540-45025-2
eBook Packages: Springer Book Archive