Com S 641 Semantic Models for Programming Languages
			     Homework: 4

E. Cohen.  Programming in the 1990s. Springer-Verlag, 1990.  Chapters 4 and 5.

The aim of this homework is to gain familiarity with specifications
and with the guarded command language.  The guarded command language
is essentially as in Dijkstra's paper, but now we'll try to do some
verification with it.

(Chapter 4)
Read this chapter quickly, paying most attention to section 4.3 and 4.4.
The material in section 4.5 is pretty much an extrapolation of 4.3 to arrays,
which are modeled as functions from integers to values (as in Com S 227 :-),
and 4.6 gives some terminology for the sorting examples in 4.7.

The following exercises require some judgement on your part,
because if we really described what you are to specify, we'd have to give
you the answer!  Therefore, make any choices you feel needed
to formalize the English description of the specification.

a. (Cohen's 4.1, p.70) Specify a program that sets x to the number of
   positive divisors of the positive integer N.  Feel free to use the
   arithmetic operator "mod".

b. (Cohen's 4.2(b), p.72) Specify a program that determines
   the number of occurrences of X in an array.
c. (Cohen's 4.5(b), p.76) Specify a program that determines
   the maximum section sum in a given integer array.
   A section of an array is informally a contiguous sequence of elements.
   See p.71 for a formal definition.  An array's section sum is the sum of the
   section's elements.
d. Do one other specification problem, of your own choosing,
   from Cohen's prblems 4.2 and 4.5.
e. (extra credit) do some more specification problems from 4.2 or 4.5.
f. (extra credit) do Cohen's exercises 4.3 and/or 4.4.


(Chapter 5)
The first exercise below is a simple example of the kind of thing
we'll study later.
g. Def: Two programs, S1 and S2, are equivalent, written S1 = S2, iff
		for all R,  wp.S1.R equiv wp.S2.R
   (Cohen's 5.1(a,b)):  Prove that, for all programs S,
		(S;skip) = S   and   (abort;S) = abort.
   This is half of the proof that skip is the unit, and abort the zero
   of composition.

You might want to do some of the easy ones in Cohen's 5.2 first.
Do more of 5.2 if you have difficulty with these; I'm happy to check more
if you want more feedback on these.  Simplify your answer as much as
possible.  Use a calculation, as on page 91!
h. (Cohen's 5.2(c)) What is wp.(x := (x-y)*(x+y)).(x + square.y = 0) ?
i. (Cohen's 5.2(d)) What is wp.(q,r := q+1,r-y).(q*y + r = x) ?
j. (Cohen's 5.4(a)) What is the following?
	wp.(if a>b -> skip [] b>a -> skip fi).true
k. (Cohen's 5.4(b)) What is the following?
	wp.(if true -> x := 2 [] true -> x := -2 fi).(x=2)
l. (extra credit) Do Cohen's problem 5.5.

Now some more semantic stuff.
m. (Cohen's 5.6) Prove: {Q} S {R} <== {Q} if B -> S fi {R}
n. (Cohen's 5.7) Prove the following equivalence of programs:
	(if B1 -> S1;S [] B2 -> S2;S fi) = (if B1 -> S1 [] B2 ->S2 fi; S)
o. (extra credit; Cohen's 5.9)
   Prove that boundedness can be guaranteed by showing that it
   holds for each guard in isolation.  That is, prove that
	(P /\ t<=0 ==> ~BB) equiv (all i : 0 <= i < n : P /\ t<=0 ==> ~B.i)
    where BB equiv (exists i : 0 <= i < n : B.i)
p. (extra credit) Do one or more of Cohen's 5.10 and 5.11