Denotational semantics do while

Denotational semantics describes the meaning of a program as some mathematical object: this is the program's denotation. Typically, the denotation of a program is a function that maps states to states. Given a program , its denotation, [[ ]], is the function that takes a state as argument and maps it to the state that results from running in the state , provided that the program terminates in the state .

The syntax of our language is described by the following BNF definitions:

::= 'a | 'b | ... | 'z | 'A | 'B | ... | 'aa | ...

::= see the first hand-out for how to define numerals

::= | | - |
+ |
*

::= < |
is |
true | false | not |
and |
or

::= skip | := |

We first give a denotational semantics for arithmetic expressions, then for Boolean expressions, and finally for programs. Before all that, we first define what we mean by a state.

State

In any imperative language, assignment is the most basic form of program: the other linguistic constructs (conditionals and loops) are simply ways of organising assignments into series that are executed in a particular order. For example, think of how (according to our intuitions) the following program is evaluated:

'x := 0 ; 'f := 1 ; while 'x ZZ. This function is defined inductively as follows:

1. For a number , clearly the value should just be , independent of the state: [[ ]](s) = n. (more precisely, we should distinguish between numerals and numbers: see the first hand-out).
   
2. For a variable , the value should simply be the value in the given state: [[ ]](s) = s(x).
   
3. When has the form e1 + e2, the value should be the sum of the values of e1 and e2: [[ e1 + e2 ]](s) = [[ e1 ]](s) + [[ e2 ]](s).
   
4. The operations for "unary minus" and multiplication are treated similarly.