Denotational Semantics

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