Abstract
Relational models for imperative programming languages provide a representation of commands in terms of binary input-output relations over states. Various relational models have arisen from modelling decisions on the distinction between angelic- and demonic nondeterminism, and have been shown to be isomorphic to disjunctive- or conjunctive predicate transformer semantics. For commands with both angelic- and demonic nondeterminism it is known that monotone unary operators provide a predicate transformer semantics but there is no conventional relational model. In this paper we propose a novel relational representation, in terms of binary multirelations, for such commands. Then we show that binary multirelations and monotone unary operators are intertranslatable.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Back, R.J.R., von Wright, J.: Refinement Calculus, part 1: Sequential Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, Springer, Heidelberg (1990)
Back, R.J.R., von Wright, J.: Combining angels, demons and miracles in program specifications. Theoretical Computer Science 100, 365–383 (1992)
Back, R.J.R., von Wright, J.: Games and winning strategies. Information Processing Letters 53(3), 165–172 (1995)
Back, R.J.R., von Wright, J.: Refinement Calclulus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)
Bell, J.L., Slomson, A.R.: Models and Ultraproducts, 2nd edn. North-Holland, Amsterdam (1971)
Brink, C.: Power structures. Algebra Universalis 30, 177–216 (1993)
Brink, C., Rewitzky, I.: A Paradigm for Program Semantics: Power Sructures and Duality. CSLI Publications, Stanford (2001)
Davey, B.A.: On the lattice of subvarieties. Houston Journal of Mathematics 5 (2), 183–192 (1979)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8), 453–458 (1975)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Gardiner, P.H., Morgan, C.C.: Data refinement of predicate transformers. Theoretical Computer Science 87 (1), 143–162 (1991)
Gardiner, P.H., Martin, C.E., de Moor, O.: An algebraic construction of predicate transformers. Science of Computer Programming 22(1-2), 21–44 (1994)
Gautam, N.D.: The validity of equations of complex algebra. Archiv. für Mathematische Logik und Grundlagenforschung 3, 117–124 (1957)
Gierz, G., Hofman, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: A Compendium of Continuous Lattices. Springer, Berlin (1980)
Hesselink, W.H.: Nondeterminism and recursion via stacks and games. Theoretical Computer Science 124, 273–295 (1994)
Hoare, C.A.R.: An algebra of games of choice, 4 p. (1996) (unpublished manuscript)
Jónsson, B., Tarski, A.: Boolean algebras with operators I. American Journal of Mathematics 73, 891–939 (1951)
Jónsson, B., Tarski, A.: Boolean algebras with operators II. American Journal of Mathematics 74, 127–167 (1952)
Morgan, C.C.: The specification statement. ACM Transactions of Programming Language Systems 10(3), 403–491 (1988)
Morgan, C.C., Robertson, K.A.: Specification statements and refinement. IBM Journal of Research and Development 31 (5) (1987)
Nelson, G.: A generalisation of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems 11 (4), 517–562 (1989)
Rewitzky, I., Brink, C.: Predicate transformers as power operations. Formal Aspects of Computing 7, 169–182 (1995)
Stone, M.H.: Topological representations of distributive lattices and Brouwerian logics. Casopis Pro Potování Mathematiky 67, 1–25 (1937)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Rewitzky, I. (2003). Binary Multirelations. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds) Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science, vol 2929. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24615-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-24615-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20780-1
Online ISBN: 978-3-540-24615-2
eBook Packages: Springer Book Archive