Com S 641 Semantic Models for Programming Languages
			     Homework: 5

E. Cohen.  Programming in the 1990s. Springer-Verlag, 1990.  Chapters 6,7

The aim of this homework is to make a few more notes about calculations,
and then to apply these to the development of correct, loopless programs.

(Chapter 6)
This chapter explains more about calculations.  Focus on what they mean
and how to prove implications.
a. (like Cohen's 6.3)  Consider a step in a calculation of the following form:
	X /\ Y /\ W
    ==>	     <hint why Y ==> Z>
	X /\ Z /\ W
   Using the definition of what a step means, state what formula has to be
   valid for this step to be valid, and prove that it is valid.
b. Which of the forms of proof of of an implication that Cohen gives
   in chapter 6 involve proving something stronger than strictly necessary?
   Which do not?  Briefly explain why for each.
c. (extra credit) Do one or more of Cohen's 6.1, 6.2, or 6.4.

(Chapter 7)
This chapter explains how to use calculations to solve for expressions in
assignments, and for guards in ifs.  It doesn't put the whole picture
of how to develop programs together.  Hang on for that, or read ahead.
d. (Cohen's 7.0)  Solve for E in each of the following:
	(a) {true} n,r := n+1,E {r = n*n}
	(b) {r = n*n} n,r := n+1,E  {r=n*n}
	(c) {r = n*n /\ s  = 2*n} n,r := n+1,E {r = n*n}
e. (extra credit) Do one or both parts of Cohen's exercise 7.1.
f. (Cohen's 7.2)  Let P be a*a <= x /\ x < b*b.  Solve for the guard B in
	   {P} if B -> a:=m fi {P}
g. (Cohen's 7.3) Let P be x > 0 and y > 0.  Solve for the guards B0 and B1 in
	{P /\ ~(x = y)}
	if B0 -> x := x - y
	[] B1 -> y := y - x
	fi
	{P}
   by first solving for B0, then for B1.
h. (extra credit) do Cohen's 7.5.