Optional: Homework # 14
due Friday, May 8, 5:00 PM

This is an optional homework is provided by request. You are under no obligation to do it. Getting a grade on this homework cannot reduce your final grade

Warning: the grade is not added to your final score, but rather will take the place of a lower Homework score (if any). It is much more beneficial to get 100% on Homework #13 than to get 50% on each of this Homework and Homework #13.

Denotational Semantics

Implement the denotational semantics from lecture in ML:

\begin{mathpar} \par {\cal E}\llbracket\texttt{$n$}\rrbracket s = n \par {\cal E... ...re } {\cal E}\llbracket\texttt{$e_1$}\rrbracket s = \textrm{inr f} \end{mathpar} You should use the following algebraic data types for expressions and values: 

datatype expr = LIT of int
              | PLUS of expr * expr
              | VAR of string
              | LET of string * expr * expr
              | FN of string * expr
              | APPLY of expr * expr
              ;

datatype value = INT of int
               | FUN of value -> value
               ;

type store = string -> value;
You should name the denotational function $\cal E$ semant and it should have type: 
semant : expr -> store -> value
Put your solution in homework14.sml.

Axiomatic Semantics

Give the weakest precondition at the beginning of this code that enables us to prove that $y \geq 0$ at the end of the following code: 

y = x;
if (y < 0) y = 0 - y; else skip
(skip is the statement that does nothing.) Show your work! Simplify the final logical expression.

Put your answer in a PLAIN ASCII TEXT file named homework14.txt.

Submitting Your Work

You submit your program work by putting it in the homework14 directory in your AFS class volume.

The homework14 directory should include the following:

About this document


John Tang Boyland 2009-05-04