About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Theoretical Computer Science
Paper
On the total correctness of nondeterministic programs
Abstract
For an arbitrary programming language with nondeterminism to be implementable, the existence of computation trees modelling the possible changes in state in the course of a computation is postulated. A general definition of what constitutes an execution method is then presented. Falling naturally out of these ideas is the correspondence between execution methods and total correctness, in that different properties are required of a program to be correct when different methods are adopted. We describe a variety of plausible methods of execution falling under the general definition and single out four particular ones. The arguments made are then illustrated by analysing the properties required by Dijkstra of guarded commands in view of these four methods. We conclude that a general approach such as that suggested here seems to be needed for dealing with programming languages and execution methods other than the particular ones treated by Dijkstra. © 1981.