Homework 2 is due before class on Monday 21 February. 1. Complete the proof that the denotational semantics is correct by showing that when (s,s') in C[c] there exists a derivation concluding with => s'. 2. [Clayton's question:] Suppose we defined the meaning of while loops as follows: C[while e do c] = U(F^i({})) where F(S) = {(s,s') | (s,0) in E[e] && s' = s} U {(s,s') | (s,i) in E[e] && i != 0 && exists s1. (s,s1) in C[c] && (s1,s') in S} i.e., without the extra "S" on the right-hand side. Show that it is still the case that C[while e do c] <= F(C[while e do c]). 3. Using the denotational semantics, show that the following programs are equivalent when run in states such that x and y are non-negative. s := 0; s := 0; while x do { while y do { s := s + y; s := s + x; x := x - 1; y := y - 1; } } That is, show that for all states s1 where s1(x) > 0 and s2(x) > 0, running the first program in s1 yields a state s2, and running the second command yields a state s2' such that s2(s) = s2'(s). 4. In the lecture notes (lecture 4) we gave 3 different potential ways to analyze while-loops using abstract stores. The first loop did not terminate and we argued informally that the third loop always terminates, but is more conservative than the second loop. Either prove that the second loop terminates or give a counter example. 5. Using analysis loop (3), prove that the analysis is sound. That is, show that for all commands c, stores s, and abstract stores S representing s, that C[c]s in C'[c]S.