Mathematics for Computer Science

Chapter 13 State Machines394

Definition 13.2.5. base cases:

 ŒŒxWDeççis the function from Env to Env defined by the rule:

ŒŒxWDeççWWDŒx ŒŒeççç:



ŒŒDoneççWWDIdEnv

where IdEnvis the identity function on Env. In other words,ŒŒDoneççWWD.

constructor cases:IfCandDarewhileprograms, andTis a test, then:



ŒŒCIDççWWDŒŒDççıŒŒCçç

That is,

ŒŒCIDççWWDŒŒDçç.ŒŒCçç/:



ŒŒifTthenCelseDççWWD

(

ŒŒCçç ifŒŒTççDT

ŒŒDçç ifŒŒTççDF:



ŒŒwhileTdoCodççWWDŒŒCçç.n/

wherenis the least nonnegative integer such thatŒŒTçç.ŒŒCçç.n//DF. (If

there is no suchn, thenŒŒwhileTdoCodççis undefined.)

We can use the denotational semantics ofwhileprograms to reason aboutwhile
programs using structural induction on programs, and this is often much simpler
than reasoning about them using induction on the number of steps in an execution.
This is OK as long as the denotational semantics accurately captures the state ma-
chine behavior. In particular, using the notation!for the transitive closure of
the transition relation:

Theorem 13.2.6.

hC; i!

̋

Done; ^0

̨

iff ŒŒCççD^0

Theorem 13.2.6 can be proved easily by induction; it appear in Problem13.1.