Com S 641 --- Semantic Models of Programming Languages

		  HOMEWORK 8: Predicate Transformers
		 (File $Date: 2002/04/19 12:38:35 $)

Due: May 1, 2002.

The following are exercises based on Chapter 11 of Back and von Wright's book.

From now on, you may abbreviate proofs as is done in the book.  In
particular it's fine to apply focusing rules, and to compress steps
involving predicate calculus.  But check each step carefully, and be
sure that it's valid, and that it is obvious how to fill in the
missing subproofs or how to expand the step into several steps.
Remember that a proof is supposed to be convincing to a skeptical
reader.  In particular, include enough detail so that you don't fool
yourself.

Please also do your proofs on the computer with an editor.  If you use
ASCII, please write write ``<='' for the refinement ordering, ``==''
for equality (=), ``==>'' for implication, ``<=='' for consequence,
``<==>'' for equivalence, ``!''  for negation, and != for inequality;
also write the quantifiers as ``(\forall v :: t)'' and ``(\exists v ::
t)'' and bounded quantification as ``(\forall v : b : t)'' and
``(\exists v : b : t)'' ``(\glb i \in I :: t)'' for greatest lower
bound, \subseteq for subset, etc.

1. (10 points) [11.1]
   Show that {p} <= [p] holds for an arbitrary predicate p.

2. (15 points) [11.2]
   Relation R is said to be total if (\forall s :: (\exists g :: R.s.g)).
   Show that [R] <= {R} holds in only if the relation R is total.

3. (20 points) [11.3]
   Prove the following properties of the test and map relations for an
   arbitrary predicate p and arbitrary function f:
       { |p| } == {p},      [ |p| ] == [p],
       { |f| } == <f>,      [ |f| ] == <f>.

4. (20 points) [11.4]
   Prove the following:
       chaos <= skip,       skip <= choose.
   Furthermore, show the quality holds if and only if the state space
   is a singleton.

5. (20 points) [11.6]
   Complete the proof of Theorem 11.4.

6. (20 points) [11.7]
   Use the assignment rules to compute the following (weakest preconditions):
      (a) (x,y := x+z, y-z).(x+y == w)
      (b) (x,y := x+z, y-z).(x == y)

7. (40 points) [11.8]
   Complete the proof of Theorem 11.3.