This section presents a constructive denotational semantics theory for a simple program language where meaning is given as a stream of states. The following definitions and theorems illustrate this library.

The data type ` Program` is built from a dozen type definitions like
those which follow.

Atomic_stmt == Abort | Skip | Assignment

Program == (depth:N # Statement(depth))

Statement(<d>) == ind(<d>; x,y.void; void; x,T. Atomic_stmt | (T#T) *concat* | (expr#T) *do loop* | expr#T#T *if then else*)

The type for stream of states, ` S`, is defined below.
Note that the ` ind` form in the definition of ` Statement`
approximates a type of trees, while ` N->State` approximates a stream
of states.
The intended meaning for ` S` is
that given an initial state, its value on
` n` is the program state after executing ` n` steps.

State* == Identifier -> Value

Done == {x:atom | x="done" in atom}

State == State* | Done <st:State> terminated == decide(<st>; u.void; u.int)

S == {f: State -> N -> State | All a:State, n:N. f(a)(n) terminated => f(a)(n+1) terminated}

Figure presents the various meaning functions as extracted objects. Using these definitions, one can define a meaning function, ` M`, for programs. This is done in figure
in the definition of ` M`, the meaning function for programs.
With ` M` one can reason about programs as well as executing them directly using the evaluation mechanism.

**Figure:** A Constructive Theory of Denotational Semantics

**Figure:** A Constructive Meaning Function for Programs

Thu Sep 14 08:45:18 EDT 1995