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.
KeywordsRandom Assignment Proof System Total Correctness Proof Outline Proof Rule
Unable to display preview. Download preview PDF.
- [Cou77]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.Google Scholar
- [Lau71]P.E. Lauer. Consistent formal theories of the semantics of programming languages. Technical Report 25.121, IBM Laboratory Vienna, 1971.Google Scholar
- [Par79]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.Google Scholar