Chapter 13 State Machines392
Executing a program causes a succession of changes to the environment^1 which
may continue until the program halts. Actually the only command which immedi-
ately alters the environment is an assignment command. Namely, the effect of the
command
xWDe
on an environment is that the value assigned to the variablexis changed to the value
ofein the original environment. We can say this precisely and concisely using the
following notation:f Œa bçis a function that is the same as the function,f,
except that when applied to elementaits value isb. Namely,
Definition 13.2.3.Iff WA!Bis a function anda;bare arbitrary elements,
define
f Œa bç
to be the functiongsuch that
g.u/D(
b ifuDa:
f.u/ otherwise.Now we can specify the step-by-step execution of awhileprogram as a state
machine, where the states of the machine consist of awhileprogram paired with
an environment. The transitions of this state machine are defined recursively on the
definition ofwhileprograms.
Definition 13.2.4.The transitionshC; i !hD; ^0 iof thewhileprogram state
machine are defined as follows:
base cases:
hxWDe; i !hDone; Œx ŒŒeçççi
constructor cases:IfCandDarewhileprograms, andTis a test, then: ifhC; i !hC^0 ; ^0 i, thenhCID; i !̋
C^0 ID; ^0
̨
:
Also,
hDoneID; i !hD; i:(^1) More sophisticated programming models distinguish the environment from astorewhich is af-
fected by commands, but this distinction is unnecessary for our purposes.