Formal semanticsContents

Formal semantics

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

Semantics domains.

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.

Semantics of expressions.

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:

Semantics of programs

We define the semantics of a program as a discrete dynamical system (S,S0, -> ) where S is the state-space of the program (see above), S0 is the set of initial states, and -> is the transition relation between states. If k0 denotes the starting point of the main procedure, then S0 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:

Formal semanticsContents