Abstract
Activating a deterministic program in a certain state will generate exactly one computation sequence. Often this level of detail is unnecessary, for example when two different computation sequences yield the same final state. The phenomenon that a program may generate more than one computation sequence from a given state is called nondeterminism.
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
K.R. Apt and E.-R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3: 65–100, 1983.
K.R. Apt and G.D. Plotkin. Countable nondeterminism and random assignment. Journal of the ACM, 33 (4): 724–767, October 1986.
K.R. Apt. Ten years of Hoare’s logic, a survey, part II: nondeter- minism Theoretical Computer Science, 28: 83–109, 1984.
J.W. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall International, Englewood Cliffs, NJ, 1980.
P. Cousot. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Technical Report Rapport de Recherche No 88, Université Scientifique et Medicale de Grenoble, L.A. 7, 1977.
E.W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18: 453–457, 1975.
E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.
R. Floyd. Nondeterministic algorithms. Journal of the ACM, 14 (3): 636–644, 1967.
M.J. Fischer and M.S. Paterson. Storage requirements for fair scheduling. Information Processing Letters, 17: 249–250, 1983.
N. Francez. Fairness. Springer-Verlag, New York, 1986.
D. Gries. The Science of Programming. Springer-Verlag, New York, 1981.
D. Gries. A note on a standard strategy for developing loop invariants and loops. Science of Computer Programming, 2: 207–214, 1982.
D.E. Knuth. The Art of Computer Programming. Vol.1: Fundamental Algorithms. Addison - Wesley, Reading, Mass., 1968.
D. König. Über eine Schlußweise aus dem Endlichen ins Unendliche. Acta Litt. Ac. Sci., 3: 121–130, 1927.
P.E. Lauer. Consistent formal theories of the semantics of programming languages. Technical Report 25.121, IBM Laboratory Vienna, 1971.
E.-R. Olderog and K.R. Apt. Fairness in parallel programs, the transformational approach. ACM Transactions on Programming Languages and Systems, 10: 420–455, 1988.
D. Park. On the semantics of fair parallelism. In D. Bjorner, editor, Proceedings of Abstract Software Specifications, pages 504–526, New York, 1979. Lecture Notes in Computer Science 86, Springer-Verlag.
A. Tarski. A lattice-theoretic fixpoint theorem and its applications. Pacific J. Math, 5: 285–309, 1955.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer Science+Business Media New York
About this chapter
Cite this chapter
Apt, K.R., Olderog, ER. (1991). Nondeterministic Programs. In: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4757-4376-0_4
Download citation
DOI: https://doi.org/10.1007/978-1-4757-4376-0_4
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4757-4378-4
Online ISBN: 978-1-4757-4376-0
eBook Packages: Springer Book Archive