Abstract
Compositional design is concerned with both constructing systems by composing components and with deconstructing systems into proposed sets of components. In bottom-up design, engineers prove system properties given properties of components and a compositional structure. In top-down design, they propose properties of components and a compositional structure given system properties. In this paper we show how the theory of predicate transformers, which has been used so successfully in sequential programming, can be applied to compositional design of systems. The rules of composition we study are more general than the rules employed in sequential programming, and the systems we study are not limited to programs. We exploit theorems about weakest and strongest solutions to equations to obtain a collection of useful predicate transformers, and then we exploit the theory of conjugate transformers to obtain more useful transformers. We show how these transformers are useful for both bottom-up and top-down design.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
MartÃn Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, January 1993.
MartÃn Abadi and Leslie Lamport. Conjoining speci_cations. ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.
MartÃn Abadi and Stephan Merz. An abstract account of composition. In Jivrà Wiedermann and Petr Hajek, editors, Mathematical Foundations of Computer Science, volume 969 of Lecture Notes in Computer Science, pages 499–508. Springer-Verlag, September 1995.
MartÃn Abadi and Gordon Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3–30, June 1993.
K. Mani Chandy and Beverly Sanders. Reasoning about program composition. Submitted for publication. http://www.cise.ufl.edu/~sanders/pubs/composition.ps.
Michel Charpentier and K. Mani Chandy. Examples of program composition illustrating the use of universal properties. In J. Rolim, editor, International workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA’99), volume1586 of Lecture Notes in Computer Science, pages 1215–1227. Springer-Verlag, April 1999.
Michel Charpentier and K. Mani Chandy. Towards a compositional approach to the design and verification of distributed systems. In J. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods in the Development of Computing Systems (FM’99),(Vol. I), volume1708 of Lecture Notes in Computer Science, pages 570–589. Springer-Verlag, September 1999.
Michel Charpentier and K. Mani Chandy. Theorems about composition. Technical Report CS-TR-99-02, California Institute of Technology, January 2000. 29 pages.
Pierre Collette. Design of Compositional Proof Systems Based on Assumption-Commitment Specifications. Application to Unity. Doctoral thesis, Faculté des Sciences Appliqués, Université Catholique de Louvain, June 1994.
Pierre Collette. An explanatory presentation of composition rules for assumption-commitment specifications. Information Processing Letters, 50:31–35, 1994.
Pierre Collette and Edgar Knapp. Logical foundations for compositional verification and development of concurrent programs in Unity. In International Conference on Algebraic Methodology and Software Technology, volume 936 of Lecture Notes in Computer Science, pages 353–367. Springer-Verlag, 1995.
Pierre Collette and Edgar Knapp. A foundation for modular reasoning about safety and progress properties of state-based concurrent programs. Theoretical Computer Science, 183:253–279, 1997.
Edsger W. Dijkstra and Carel S. Scholten. Predicate calculus and program semantics. Texts and monographs in computer science. Springer-Verlag, 1990.
J.L. Fiadeiro and T. Maibaum. Verifying for reuse: foundations of object-oriented system verification. In I. Makie C. Hankin and R. Nagarajan, editors, Theory and Formal Methods, pages 235–257. World Scientific Publishing Company, 1995.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
Rob T. Udink. 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., Mani Chandy, K. (2000). Reasoning about Composition Using Property Transformers and Their Conjugates. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds) Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics. TCS 2000. Lecture Notes in Computer Science, vol 1872. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44929-9_40
Download citation
DOI: https://doi.org/10.1007/3-540-44929-9_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67823-6
Online ISBN: 978-3-540-44929-4
eBook Packages: Springer Book Archive