On the total correctness of nondeterministic programs

AbstractFor 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