Concepts of Programming Languages

378 Chapter 8 Statement-Level Control Structures

Now, consider this same process coded in a traditional programming language

selector:

if (x >= y)

max = x;

else

max = y;

This could also be coded as follows:

if (x > y)

max = x;

else

max = y;

There is no practical difference between these two statements. The first assigns

x to max when x and y are equal; the second assigns y to max in the same

circumstance. This choice between the two statements complicates the formal

analysis of the code and the correctness proof of it. This is one of the reasons

why guarded commands were developed by Dijkstra.

The loop structure proposed by Dijkstra has the form

do <Boolean expression> -> <statement>

[] <Boolean expression> -> <statement>

[]...

[] <Boolean expression> -> <statement>

od

The semantics of this statement is that all Boolean expressions are evaluated

on each iteration. If more than one is true, one of the associated statements

is nondeterministically (perhaps randomly) chosen for execution, after which

the expressions are again evaluated. When all expressions are simultaneously

false, the loop terminates.

Consider the following problem: Given four integer variables, q1, q2, q3,

and q4, rearrange the values of the four so that q1 ≤ q2 ≤ q3 ≤ q4. Without

guarded commands, one straightforward solution is to put the four values into

an array, sort the array, and then assign the values from the array back into

the scalar variables q1, q2, q3, and q4. While this solution is not difficult, it

requires a good deal of code, especially if the sort process must be included.

Now, consider the following code, which uses guarded commands to solve

the same problem but in a more concise and elegant way.^7

do q1 > q2 -> temp := q1; q1 := q2; q2 := temp;

[] q2 > q3 -> temp := q2; q2 := q3; q3 := temp;

7. This code appears in a slightly different form in Dijkstra (1975).