Optional: Homework # 14
due Tuesday, May 10, 3:30 PM

This is an optional homework. You are under no obligation to do it. The grade on this homework will take the place of a lower homework score (if any).

Denotational Semantics

Implement the denotational semantics from lecture in ML: \begin{mathpar} \par {\cal E}\llbracket\texttt{$n$}\rrbracket m = n \par {\cal E... ...et m}\right) \par {\cal E}\llbracket\texttt{$x$}\rrbracket m = m x \end{mathpar} \begin{mathpar} {\cal S}\llbracket\texttt{skip}\rrbracket m = (m,()) \par {\cal ... ...{if $e$\ > 0 then skip else $s$; until $e$\ > 0 do $s$}\rrbracket \end{mathpar}

You should use the following algebraic data types for expressions and statements: 

datatype expr = LIT of int
              | PLUS of expr * expr
              | TIMES of expr * expr
              | VAR of string
              ;

datatype stmt = SKIP
              | ASSIGN of string * expr
              | SEQ of stmt * stmt
              | PRINT of expr
              | IFPOS of expr * stmt * stmt
              | UNTILPOS of expr * stmt
              ;

type memory = string -> int;
type output = int list;

You should name the denotational functions $\cal E$ and $\cal S$ sExpr and sStmt respectively. they should have type: 

sExpr : expr -> memory -> int
sStmt : stmt -> memory -> memory * output
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
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 2011-05-06