Com S 641 Semantic Models for Programming Languages
			     Homework: 9

Wim Hesselink.  Programs, Recursion and Unbounded Choice. Cambridge, 1992.

a. Add a syntax for functions to Hesselink's language.
   Give a formal semantics (a la Hesselink).  (Part of the problem is to
   figure out what it means to give a formal semantics to such a feature.)
   You will have to make various design decisions (such as: can functions
   have side-effects? can they have var-parameters?  etc.).
   Can you offer some kind of proof that your semantics is correct?
   Briefly discuss why you think Hesselink omitted program functions.

b. (extra credit only) Add a syntax for blocks with local declarations
   to Hesselink's language.  Give a formal semantics for it.

c. Read a paper about about axiomatic semantics and write a short review of it.
   (By short I mean, roughly 1 page, perhaps less, not too much more.)
   You can find suggestions in the handout I passed out at the beginning
   of the semester, or in the bibliography in Hesselink's book.
   In your review, be sure to summarize:
	* the problem addressed by the paper
	* the solution offered by the paper
	* what you thought was new (at the time), important, or particularly
		interesting
	* in what ways it differs from or is similar to Hesselink's approach,
	  and in what ways you think the differences are better or worse.

(Chapter 3)
The main point of this chapter is technical: to introduce the two healthiness
laws on the predicate transformers wp and wlp,
and to explore some of their implications.

(section 3.2)
d. Do Hesselink's 3.2.0.  What, in words, is the command `c' of this exercise?

(section 3.3)
e. Do Hesselink's 3.3.0.
f. Do Hesselink's 3.3.1.
g. Do Hesselink's 3.3.2.
h. (extra credit only) Do Hesselink's 3.3.3.

(section 3.5)
i. (extra credit only) Do Hesselink's 3.5.1.
j. Do Hesselink's 3.5.2.