Abstract
In this paper we present the ImpUNITY framework, a framework that supports the development of parallel and distributed programs from specification to implementation in a stepwise manner. The ImpUNITY framework is an extension of UNITY, as introduced by Chandy and Misra, with features of the Action System formalism of Back and Kurki-Suonio. Due to this extension, the ImpUNITY framework is more suitable for the implementation phase of the develop process. It supports local variables and (remote) procedure calls. has a UNITY like temporal logic.
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.
This research has been supported by the Foundation for Computer Science in the Netherlands SION under project 612-317-107.
Preview
Unable to display preview. Download preview PDF.
References
R.-J.R. Back. Refinement calculus, part II: Parallel and reactive programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 42–66. Springer-Verlag, 1990.
R. J.R. Back. Refinement calculus, lattices and higher order logic. In M. Broy, editor, Program Design Calculi, volume 118 of Nato ASI Series, Series F, pages 53–72. Springer-Verlag, 1993.
R.J.R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In 2nd ACM SIGACT-SIGOPS Symp. on Distributed Computing, pages 131–142. ACM, 1983.
R.J.R. Back and K. Sere. Action systems with synchronous communication. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi, volume A-56 of IFIP Transactions, pages 107–126. IFIP, Elsevier Science Publishers B.V. (North Holland), June 1994.
R.J.R. Back and J. van Wright. Duality in specification languages: A latticetheoretical approach. Acta Informatica, 27:583–625, 1990.
K.M. Chandy and J. Misra. Parallel Program Design — A Foundation. Addison-Wesley Publishing Company, Inc., 1988.
J. Pachl. A simple proof of a completeness result for leads-to in the UNITY logic. Information Processing Letters, 41:35–38, 1992.
B.A. Sanders. Stepwise refinement of mixed specifications of concurrent programs. In M. Broy and Jones C.B., editors, Proceedings of the IFIP Working Conference on Programming and Methods, pages 1–25. Elsevier Science Publishers B.V. (North Holland), May 1990.
B.A. Sanders. Eliminating the substitution axiom from UNITY logic. Formal Aspects of Computing, 3(2):189–205, 1991.
Ambuj K. Singh. Program refinement in fair transition systems. Acta Informatica, 30(6):503–535, 1993.
R.T. Udink, T. Herman, and J.N. Kok. Progress for local variables in UNITY. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi, volume A-56 of IFIP Transactions, pages 127–146. IFIP, Elseviers Science Publishers B.V. (North Holland), June 1994.
R.T. Udink and J.N. Kok. Two fully abstract models for UNITY. In Eike Best, editor, CONCUR'93, Proceedings of the 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 339–352. Springer-Verlag, August 1993.
R.T. Udink and J.N. Kok. The Dagstuhl specification problem, UNITY-Refinement Calculus. Presentation at the Dagstuhl Seminar on Reactive Systems, September 1994. http://www.research.digital.com/SRC/personal/Leslie-Lamport/dagstuhl/all.html
J. von Wright. The lattice of data refinement. Acta Informatica, 31(2):105–135, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Udink, R.T., Kok, J.N. (1995). ImpUNITY: UNITY with procedures and local variables. In: Möller, B. (eds) Mathematics of Program Construction. MPC 1995. Lecture Notes in Computer Science, vol 947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60117-1_24
Download citation
DOI: https://doi.org/10.1007/3-540-60117-1_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60117-3
Online ISBN: 978-3-540-49445-4
eBook Packages: Springer Book Archive