This assignment is worth **20%** of the
overall mark for the module SE424 Program Language Design.

Please submit your assignment solutions to
Rosemary (2.105, Callan Extension) before **5pm on Friday 12 ^{th} December 2003.** Please
include both a hard and soft copy of your code.

__Part 1: Background Notation
(25 marks)__

Using the operator defined in lectures, simply the following where identifiers m,n Î Nat, t Î Tr,

p Î Tr x Tr,
r Î Tr + Nat, and x,y Î Nat_{^} . Explain each step of the simplification process.

(a) (lp.(snd p, fst p )) (true, (two equals one))

(b) ((lr.cases r of isTr (t) ® (lm.zero) [] isNat(n) ® (lm.n) end) (inNat (two))) (one)

(c) cases (false ® inNat(one) [] inTr(false)) of isTr (t) ® true or t [] isNat(n) ® false end

(d) (lx. (lm.m equals zero ® x [] one ) (two)) (^)

(e) let m = (lx.x) zero in let n = (m equals zero ® one [] ^)in m plus n

(a) Using the denotational definition of an imperative language (Figure 5.2) from your lecture notes, code (in C++ /Java) a test implementation of the language described. Clearly document the following through code comments and additional notes:

· what the semantic algebra’s become in the implementation

· how the valuation equations are realised

· what the store becomes

· what information the denotational definition does not provide for your implementation.

(b) Extend the program you have just written so that it can take two programs as input, calculate their denotations and hence determine whether the two programs are equivalent. Discuss any limitations/ problems that encountered in achieving this.

__ __

(a) Identify any problems that you see with implementing the following extension of the language definition defined in Figure 5.2 of your lecture notes:

C[test E on C] = l
s. let s’ = C[C]s in E[E]s’ equals zero ®s’[]s

Suggest an improved valuation function for the command test E on C and implement this in your program from Part 2 above.

(b) Extend the language of Figure 5.2 with a parallel assignment command so that commands such as

[ I, J:= 0,1]
result in the simultaneous update of identifiers I and J. Explain why the
following valuation function is not sufficient as a solution:

C[I1, I2 := E1, E2] =

__l__
s. let s’ = (update [I1] E[E1]s s) in
update ([I2] E [E2]s’ s’)