13.2. Reasoning AboutWhilePrograms 391
CID—called thesequencingofCandD, ifTthenCelseD—called aconditionalwithtest,T, andbranches,Cand
D, whileTdoCod—called awhile loopwithtest,T, andbody,C.For simplicity we’ll stick towhileprograms operating on integers. So by expres-
sions we’ll mean any of the familiar integer valued expressions involving integer
constants and operations such as addition, multiplication, exponentiation, quotient
or remainder. Astests, we’ll allow propositional formulas built from basic formu-
las of the formef whereeandf are expressions. For example, here is the
Euclidean algorithm for gcd.a;b/expressed as awhileprogram.
xWDa;
yWDb;
whiley¤ 0 do
tWDy;
yWDrem.x;y/;
xWDtod
13.2.2 The While Program State Machine
Awhileprogram acts as a pure command: it is run solely for its side effects on
stored data and it doesn’t return a value. The data consists of integers stored as the
values of variables, namely environments:
Definition 13.2.2.Anenvironmentis a total function from variables to integers.
Let Env be set of all environments.
So ifis an environment andxis a variable, then.x/is an integer. More
generally, the environment determines the integer value of each expression,e, and
the truth value of each test,T. We can think of an expression,eas defining a
functionŒŒeççWEnv!Z, and refer to this function,ŒŒeçças themeaningofe, and
likewise for tests.
It’s standard in programming language theory to writeŒŒeçças shorthand for
ŒŒeçç./, that is, applying themeaning,ŒŒeçç, ofeto. For example, if.x/D 4 , and
.y/D 2 , then
ŒŒx^2 Cy 3 ççD.x/^2 C.y/ 3 D11: (13.3)