Chapter 13 State Machines390
mis the first message onwork-buf 1. The effect of the transition is to changetag 2
to make it equal totag 1 , and to replicate the first element ofwork-buf 221 at the
end ofbuf 2.
The inductive hypothesis implies that, before the step,buf 2 work-buf 1 D
buf 1. The changes caused by the step imply that, after the step,tag 1 D tag 2 ,
work-buf 1 andbuf 2 are nonempty,head.work-buf 1 / Dlast.buf 2 /, andbuf 2
tail.work-buf 1 /Dbuf 1. This is as needed.
receive.b/2;1:
The argument is similar to the one forreceive.m;b/1;2. Ifb¤tag 1 , nothing
happens so the invariants are preserved. So suppose thatbDtag 1. Then Property
2 implies thatbDtag 2 , and the step changestag 1 to make it unequal totag 442.
The step also removes the first element ofwork-buf 1. The inductive hypothesis im-
plies that, before the step,work-buf 1 andbuf 2 are nonempty,head.work-buf 1 /D
last.buf 2 /, andbuf 2 tail.work-buf 1 /Dbuf 1. The changes caused by the step
imply that, after the step,tag 1 ¤tag 2 andbuf 2 work-buf 1 Dbuf 1. This is as
needed.
13.2 Reasoning AboutWhilePrograms
Real programs and programming languages are often huge and complicated, mak-
ing them hard to model and even harder to reason about. Still, making programs
“reasonable” is a crucial aspect of software engineering. In this section we’ll illus-
trate what it means to have a clean mathematical model of a simple programming
language and reasoning principles that go with it—if only real programming lan-
guages allowed for such simple, accurate modeling.
13.2.1 While Programs
The programs we’ll study are called “whileprograms.” We can define them as a
recursive data type:
Definition 13.2.1.
base cases:
xWDeis awhileprogram, called anassignment statement, wherexis a
variable andeis an expression.
Doneis awhileprogram.
constructor cases:IfC andDarewhileprograms, andT is a test, then the
following are alsowhileprograms:
