Advertisement
Published in:
2009 | OriginalPaper | Chapter
Nondeterministic Programs
Published in: Verification of Sequential and Concurrent Programs
Publisher: Springer London
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In The Previous chapters we have seen that parallel programs introduce nondeterminism: from a given initial state several computations resulting in different final states may be possible. This nondeterminism is implicit; that is, there is no explicit programming construct for expressing it. In this chapter we introduce a class of programs that enable an explicit description of nondeterminism. This is the class of Dijkstra's [1975,1976]
guarded commands;
it represents a simple extension of
while
programs considered in Chapter 3. Dijkstra's guarded commands are also a preparation for the study of distributed programs in Chapter 11.