Abstract
We show how to introduce demonic and angelic nondeterminacy into the term language of each type in typical programming or specification language. For each type we introduce (binary infix) operators ⊓ and ⊔ on terms of the type, corresponding to demonic and angelic nondeterminacy, respectively. We generalise these operators to accommodate unbounded nondeterminacy. We axiomatise the operators and derive their important properties. We show that a suitable model for nondeterminacy is the free completely distributive complete lattice over a poset, and we use this to show that our axiomatisation is sound. In the process, we exhibit a strong relationship between nondeterminacy and free lattices that has not hitherto been evident. Although nondeterminacy arises naturally in specification and programming languages, we speculate that it combines fruitfully with function theory to the extent that it can play an important role in facilitating proofs of programs that have no apparent connection with nondeterminacy.
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.
References
Back, R.-J., von Wright, J.: Refinement Calculus: a Systematic Introduction. Springer, Heidelberg (1998)
Bartenschlager, G.: Free bounded distributive lattices over finite ordered sets and their skeletons. Acta Mathematica Universitatis Comenianae 64, 1–23 (1995)
Birkhoff, G.: Lattice Theory. American Mathematical Society, vol. 25. Colloquium Publications (1995)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Freese, R., Jezek, J., Nation, J.B.: Free Lattices, American Mathematical Society. Mathematical Surveys and Monographs, vol. 42 (1995)
Ganter, B., Wille, R.: Formal Concept Analysis. Springer, Heidelberg (1999)
Hehner, E.C.R.: A Practical Theory of Programming. Springer, New York (1993) ISBN 0387941061
Markowsky, G.: Free completely distributive lattices. Proceedings of the American Mathematical Society 74, 227–228 (1979)
Morris, J.M., Bunkenburg, A.: Specificational functions. ACM Transactions on Programming Languages and Systems 21, 677–701 (1999)
Morris, J.M., Bunkenburg, A.: A Theory of Bunches. Acta Informatica 37, 541–561 (2001)
Norvell, T.S., Hehner, E.C.R.: Logical specifications for functional programs. In: Bird, R.S., Woodcock, J.C.P., Morgan, C.C. (eds.) MPC 1992. LNCS, vol. 669, pp. 269–290. Springer, Heidelberg (1993)
Spivey, J.M.: Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press, Cambridge (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Morris, J.M. (2004). Augmenting Types with Unbounded Demonic and Angelic Nondeterminacy. In: Kozen, D. (eds) Mathematics of Program Construction. MPC 2004. Lecture Notes in Computer Science, vol 3125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27764-4_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-27764-4_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22380-1
Online ISBN: 978-3-540-27764-4
eBook Packages: Springer Book Archive