Abstract
This chapter presents the core of SESF theory in four parts. First, it defines what it means for program A to implement program B in terms of the evolutions of A and B. Second, it establishes compositionality: if program A implements program B, then replacing an instantiation of B in any program C by an instantiation of A preserves all the properties of program C. Third, it presents the program version of “A implements B” for the case where B is a service program without internal parameters. Briefly, A implements B iff the composite system of A and B-inverse satisfies B-inverse’s input conditions and progress condition. Fourth, it extends the program version of “A implements B” to the case where B is a service program with internal parameters, essentially by converting the internal parameters into external parameters.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
M. Abadi, L. Lamport, The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253–284 (1991). doi:10.1016/0304-3975(91)90224-P. http://dx.doi.org/10.1016/0304-3975(91)90224-P
M. Abadi, L. Lamport, Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993). doi:10.1145/151646.151649. http://doi.acm.org/10.1145/151646.151649. Also in Stepwise Refinement of Distributed Systems, LNCS 430, Springer-Velag, 1990
R. johan Back, J.V. Wright, Contracts, games, and refinement. Inf. Comput. Control 156, 25–45 (2000). doi:10.1006/inco.1999.2820
R.J.R. Back, F. Kurki-Suonio, Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988). doi:10.1145/48022.48023. http://doi.acm.org/10.1145/48022.48023
R.J.R. Back, R. Kurki-Suonio, Decentralization of process nets with centralized control, In: Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, PODC ’83. (ACM, New York, 1983), pp. 131–142. doi:10.1145/800221.806716. http://doi.acm.org/10.1145/800221.806716
R.J.R. Back, K. Sere, Stepwise refinement of parallel algorithms. Sci. Comput. Program. 13(2–3), 133–180 (1990). doi:10.1016/0167-6423(90)90069-P. http://dx.doi.org/10.1016/0167-6423(90)90069-P
K.M. Chandy, J. Misra, An example of stepwise refinement of distributed programs: quiescence detection. ACM Trans. Program. Lang. Syst. 8(3), 326–343 (1986). doi:10.1145/5956.5958. http://doi.acm.org/10.1145/5956.5958
K.M. Chandy, J. Misra, Parallel Program Design: A Foundation (Addison-Wesley, Reading, 1989)
S.S. Lam, A.U. Shankar, Specifying modules to satisfy interfaces: a state transition system approach. Distrib. Comput. 6(1), 39–63 (1992). doi:10.1007/BF02276640. http://dx.doi.org/10.1007/BF02276640
L. Lamport, Specifying concurrent program modules. ACM Trans. Program. Lang. Syst. 5(2), 190–222 (1983). doi:10.1145/69624.357207. http://doi.acm.org/10.1145/69624.357207
L. Lamport, A simple approach to specifying concurrent systems. Commun. ACM 32(1), 32–45 (1989). doi:10.1145/63238.63240. http://doi.acm.org/10.1145/63238.63240
L. Lamport, The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994). doi:10.1145/177492.177726. http://doi.acm.org/10.1145/177492.177726
N.A. Lynch, M.R. Tuttle, Hierarchical correctness proofs for distributed algorithms, in Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, PODC ’87 (ACM, New York, 1987), pp. 137–151. doi:10.1145/41840.41852. http://doi.acm.org/10.1145/41840.41852
Z. Manna, A. Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comput. Program. 4(3), 257–289 (1984). doi:10.1016/0167-6423(84)90003-0. http://dx.doi.org/10.1016/0167-6423(84)90003-0
A.U. Shankar, S.S. Lam, A stepwise refinement heuristic for protocol construction. ACM Trans. Program. Lang. Syst. 14(3), 417–461 (1992). doi:10.1145/129393.129394. http://doi.acm.org/10.1145/129393.129394. Earlier version appeared in Stepwise Refinement of Distributed Systems, LNCS 430, Springer-Verlag, 1990
K. Suonio, A Practical Theory of Reactive Systems: Incremental Modeling of Dynamic Behaviors (Springer, Secaucus, 2005). (Texts in Theoretical Computer Science. An EATCS Series)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer Science+Business Media New York
About this chapter
Cite this chapter
Shankar, A.U. (2013). Implements and Compositionality. In: Distributed Programming. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-4881-5_7
Download citation
DOI: https://doi.org/10.1007/978-1-4614-4881-5_7
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4614-4880-8
Online ISBN: 978-1-4614-4881-5
eBook Packages: Computer ScienceComputer Science (R0)