2.   In class we gave a denotational semantics to a simple imperative language.  The semantics we gave interpreted expressions as functions from states to integer values.  It also interpreted statements as functions from states to states.  A state (or memory) was a mapping from variables to values.  

Denotational semantics are often used in a kind of program analysis referred to as "abstract interpretation."  The idea of abstract interpretation is that you do not necessarily need to find out the exact answer of a question.  You only need to find out an approximate (or abstract) answer.  Abstract interpretation can be used to optimize programs and also to verify simple properties of programs.  So, in this question we will develop a different, "more abstract" semantics for expressions and statements.  This more abstract semantics will not compute the exact answer, but it will compute some useful information. 

Here is the syntax of a slightly revised version of the imperative programming language we looked at in class.  In particular, notice that our collection of statements includes a statement "declare t x in s".  This declares a new variable x that may be used within the statement s, but does not initialize it.  Initialization may be done at some later point using an assignment statement: x:= e.  The operation "=b" tests for equality of booleans.  The operation "=i" tests for equality of integers.  The operation e1 ? e2 : e3 evaluates e1 to a boolean.  If true, executes e2.  If false, executes e3.   

values v ::= n | true | false

operators op ::= + | - | > | =i | =b

types t ::= int | bool

expressions e ::=  x | n | true | false | e op e | e ? e : e

statements s ::= declare t x in s | x := e | s ; s | if e then s else s | while e do s

a)  [5 points] Your job is to give an abstract denotational semantics of these programs.  More specifically, your denotational semantics will NOT compute the exact meaning of expressions or statements, but instead, it will compute their types.  In some sense you will be developing a type checker function for these programs.  However, your type checker will also need to take care of checking that variables are not used to before they are initialized.

Your denotational definition for expressions and statements will have this form:

[[e]]state = t or BAD

[[s]]state = state or BAD

"BAD" will indicate that an uninitialized variable may have been dereferenced, an undeclared variable used, or the program is otherwise ill-typed. 

"state"  is a function from variables to "abstract values" and abstract values are defined here:

abstract values a ::= int | bool | ?int | ?bool

Your denotational definition must have the following properties.  These aren't necessarily a complete list of properties your definition should have.  If you are unsure, you can always e-mail the class list and ask.

1. If [[e]]state = int then then it should be the case that e does not use any uninitialized variables and it always produces an integer value (as opposed to a boolean value)

2. If [[e]]state = bool then it should be the case that e does not use any uninitialized variables and it always produces an boolean value (as opposed to an integer value)

3. If [[e]]state = BAD then e might use uninitialized values (and it might not -- it will not be possible to deterimine this property exactly). Alternatively, the denotation of an expression should be BAD if the expression is not well-typed in the usual sense.

4. If [[s]]state = BAD then s might use uninitialized values (and it might not) or s might try to assign to variables that have not been declared.  Alternatively, the denotation of an expression should be BAD if the expression is not well-typed in the usual sense (if you have questions about that, feel free to ask).   

5. If [[s]]state = state' then s will definitely not refer to uninitialized variables.  If s is executed in starting in a real program memory satisfying the properties of "state" the result would be a real program memory satisfying the properties of "state'."  In other words, if state'(x) = int, then after execution of s, x will definite contain an integer. If state'(x) = ?int, then after execution of s, x may contain an integer, but may also be uninitialized.

6.  Your definitions must be implementable and decidable.  You potentially have to be careful when defining your abstract interpretation over while loops.  Be sure that to implement your definitions you do not potentially have to loop forever when analyzing a while loop.

b) [5 points] Implement the syntax of the language above in ML (use ML datatypes and some representation of variables).  Implement your denotational semantics definitions in ML.  Show 2 or 3 representative example programs and the output of your semantic checker on them.