## Formal semantics

We give here the standard operational semantics of the "Simple"
language.

They are summarized by the following table:

An environment is defined by a function assigning a value to a set
of variables *Var* visible in the current scope.
A program state is a non-empty stack of activation records. A
stack is viewed as a word where the last letter corresponds to the
top of the stack.

The semantics of a numerical expression `nexpr`
is a function

We refer to [1] for the precise definition of this semantic
function.
The semantics of a Boolean expression `bexpr`
is a function

which is defined inductively as follows:

The semantics of a Boolean expression can be extended as a predicate on environments as follows:

We define the semantics of a program as a discrete dynamical
system *(S,S*_{0}, -> ) where *S* is the state-space of the
program (see above), *S*_{0} is the set of initial states, and
* -> * is the transition relation between states.
If *k*_{0} denotes the starting point of the main procedure, then *S*_{0} is defined as

This reflects the hypothesis that variables are uninitialized
(read: they may contain arbitrary values) at start.
The transition relation is defined as follows: