This assignment has 25 points.
|1. Read Pierce, chapter
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.
2. Semantics of pictures.
val cmd = String.concat ["display ",tmp_file]
(* FOR WINDOWS, REPLACE PREVIOUS LINE WITH THIS ONE:
val cmd = String.concat ["imdisplay ",tmp_file] *)
fun showIt area p = Convert.display area (pict2image p)
(** Uncomment if you are having problems with your display. Your program will then create
the file output.png, which you may view with a generic tool.
For instance, Windows picture and fax viewer will work. **)
(* fun showIt area p = pict2PNG area p "ouput.png" *)
(** Uncomment for quick debugging *)
(* fun showIt area p = pict2ASCII area p *)
Your job is to read and understand the document on the semantics of pictures. Once you understand the semantics, you should complete the file shape.sml. This involves completing the following components.
a) [2 points] Complete the cases of the deno
function that are related to the primitive shapes Elipse and
HalfPlane. After completing the cases you should be able to run the tests Test.test circle and
Test.test half plane.
b) [3 points] Complete the cases of the deno
function that are related to the primitive shapes Intersect,
Union, and Diff. After completing the cases you should be able to run the tests Test.test_hole and
c) [2 points] Complete the cases of the deno
function that implement the cases related to Trans and
ScaleXY. After completing the cases you should be able to run the tests Test.test_letter_e and
d) [4 points] Complete the function remove_trans. The function remove_trans should rewrite a shape definition into a shape definition that does not contain any Trans operations. To figure out how to implement this function, use the equations discussed in the document on our semantics of shapes. Do your own debugging.
e) [4 points] Complete the function remove_scale. The function remove_scale should rewrite a shape definition into a shape definition that does not contain any scaleXY operations. To figure out how to implement this function, use the equations discussed in the document on our semantics of shapes. Do your own debugging.