ether with an intuitive (mechanistic) definition of their
semantics. The basic building block for both of them
is the so-called "guarded command," a statement list
prefixed by a boolean expression: only when this
boolean expression is initially true, is the statement list
eligible for execution. The potential nondeterminacy
allows us to map otherwise (trivially) different programs
on the same program text, a circumstance that seems
largely responsible for the fact that programs can now
be derived in a manner more systematic than before.
In Section 3, after a prelude defining the notation,
a formal definition of the semantics of the two constructs is given, together with two theorems for each
of the constructs (without proof).
In Section 4, it is shown how, based upon the above,
a formal calculus for the derivation of programs can
be founded. We would like to stress that we do not
present "an algorithm" for the derivation of programs:
we have used the term "a calculus" for a formal discipline--a set of rules--such that, if applied successfully:
(1) it will have derived a correct program; and (2) it
will tell us that we have reached such a goal. (We use
the term as in "integral calculus.")