skip
fail
if B then P1 else P2 fi
μX (P)
while B do P od
is short for
is short for
is short for
is short for
is short for
true?
false
(B?; Pi) ∪ (-B?; P2)
hX ^ P i(X)
μX((B?; P; X) ∪-B?)
Remark on notation. The sequence operator “;” is associative, both on its
intuitive interpretation (Pi; P2 meaning “do Pi and then P2”) and given the
semantics (relational composition) it gets in this paper and elsewhere. We
shall also make no syntactic distinction between (Pi; P2); P3 and Pi; (P2; P3)
and write both as Pi ; P2; P3. Similarly, we syntactically identify P with
skip; P and with P;skip. This is allowed because skip intuitively means
“do nothing” and will be interpreted formally as the diagonal relation {hi, ii |
i is a state}. The identification will allow us to say that the programs Pi ; P
and P; P2 , as well as the program P, have the form Pi ; P; P2: we can take
Pi or P2 or both to be the identity element skip.
An occurrence of a program variable Y ∈ {Xi , . . . , Xn} is free in a program
P if it does not occur within a subprogram of the form hXi ^ Piin=1(P0) in
P . A program is closed if it contains no free program variables.
Our procedure declarations can bind a series of program variables simul-
taneously, and since procedure declarations may make mutual calls it will not
be possible to reduce this form of binding to an iteration of bindings, as it
can usually be done in logic. Since we shall also have occasion to work with
simultaneous substitutions, things threaten to get a bit complicated. The
following definition may look a bit hairy, but in fact gives a straightforward
generalisation of the usual notion of substitution.
Definition 3 (Substitution) The simultaneous substitution [Pi/Xi]in=1P
of P1 for X1 and . . . and Pn for Xn in P (abbreviated as [Pi/Xi]iP) is defined
as follows.
[Pi/Xi]iXk = Pk, if 1 ≤ k≤n
[Pi/Xi]iA = A, ifA∈/ {X1,...,Xn}
[Pi/Xi]i(Q1; Q2) = [Pi/Xi]i Q1; [Pi/Xi]iQ2
[Pi∕Xi]i(Qι ∪ Q2) = [Pt∕Xi]i Qi ∪ [Pi∕Xi]i Q2