Com S 641 Semantic Models for Programming Languages
			     Homework: 7

Wim Hesselink.  Programs, Recursion and Unbounded Choice. Cambridge, 1992.
Chapters 0,1

This homework lays the foundation for our study of Hesselink's monograph.
We see Hesselink's language, and look at why it differs from Dijkstra's
guarded command language.  This is a good time to develop or practice your
skills of critical reading of a mathematically dense text.
When you don't understand something, try rereading the last part you read.
Keep asking questions as you read, especially: is that true? why is this being
considered?  is there any other way to do that?  (Of course, I will be happy
to discuss questions during class and in my office as well.)

(Chapter 0)
In reading this chapter pay attention especially to sections 0.0-0.2,
and 0.6-0.7.  You can skim quickly over 0.3-0.5.  In sections 0.0 and 0.6
pay most attention to notational issues, and in 0.1, 0.2, and 0.7
pay most attention to why Hesselink is considering various things.

(Chapter 1)
This chapter covers absolutely fundamental concepts, and notation,
especially the language that Hesselink uses.  However, much of it will
be, or should be familiar to you by now.  You might consider doing Hesslink's
proofs yourself first, without looking at the book, as this helps you
understand better what he is doing.
(Section 1.1)
a. Hesselink's exercise 1.1.1 (Hint: use a format for proving an implication
   where you assume the hypothesis in a step.)
b. Hesselink's 1.1.2
c. Hesselink's 1.1.4
aa. What is the connection between ~[p] and [~p]?  Prove it.
e. Hesselink's 1.1.7
d. Hesselink's 1.1.5
(Section 1.2)
f. Recall the command "havoc" which is guaranteed to terminate but which is
   nondeterministic to such an extent that it can terminate in every possible
   state.  Define wp.havoc.p and wlp.havoc.p.
(Section 1.3)
g. Hesselink's 1.3.0
h. What are the connections, if any, between wp.(?b;c).p, wlp.(?b;c).p and the
   total and partial correctness Hoare triples {b} c {p} and b {c} p?
(Section 1.4)
i. Hesselink's 1.4.0(b). Also: why isn't it always true that c;abort =~= abort?
   (Here =~= means semantic equality of commands (Formula 7).)
j. Hesselink's 1.4.1(b)
k. Hesselink's 1.4.2
l. Hesselink's 1.4.3
m. Hesselink's 1.4.4
(Section 1.5)
n. Hesselink's 1.5.0
(Section 1.6)
o. Hesselink's 1.6.0
(Section 1.7)
p. Hesselink's 1.7.0
(Section 1.8)
q. Hesselink's 1.8.0