Com S 641 Semantic Models for Programming Languages
			     Homework: 1

E.W. Dijkstra. Guarded Commands, Nondeterminacy and Formal Derivation
of Programs.  CACM, 18(8):453-457, 1975.

(Section 2)
a. Dijkstra doesn't give syntax for boolean expressions, or "other statements".
   Does that bother you when reading the paper?  What does this say about
   writing technical papers?
b. Explain how the program on the bottom left of page 454 works.
c. Why (informally) is Dijkstra's claim in the last sentence before
   section 3 true?  What assumptions are being made about f?

(Section 3)
(Section 3.1)
By the "state space" Dijkstra means (informally) all the variables
in the program.  Take careful note of the first 3 paragraphs in section 3.1;
we'll be exploring this idea for most of the semester!
d. Hoare said that ignoring termination led to more machine independence
   in reasoning (proofs of correctness).  Do you think Dijkstra is worried
   that his proofs will be more complex?  If not, why not?
e. Why is the "Law of the Excluded Miracle" called that?
f. Why is the forth property (bottom of page 454 to top of page 455)
   restricted to deterministic statements?
g. What does the "note" in the third full paragraph of page 455 mean?
   Why is it there?
h. Is example 2 defining whether side-effects may occur in expressions?
   Or is it assuming something about side-effects?
i. Can you state formally an interesting relationship between hoare triples
   and Dijkstra's weakest precondition transformers.  (Hint: you might want
   to use an implication.)
(Section 3.2)
j. Prove theorem 1.  (extra credit: prove theorem 2)
(Section 3.3)
In section 3.3, note that "non" is the boolean negation operator,
and that the notation of the two colons in the existential can be read
as "such that...and".  We'll see more of the latter notation in Cohen.
k. How does Dijkstra's semantics for "the repetitive construct" compare
   to Hoare's?  Which theorem is like Hoare's rule for while loops?
   Why is the other theorem there?  What is the relationship of these
   theorems to the weakest precondition?  (That is, are they necessary?
   sufficient?)

(Section 4)
l. What is Dijkstra saying about how you should think about programming
   in these examples?
m. Why does Dijkstra think that having fewer ways to write a particular
   program (page 457) is a good idea?

(Section 5)
n. Is the question Dijkstra asks in the second paragraph an interesting one
   to you?

(General questions)
o. How would you summarize the contribution of this paper in a few sentences?
p. Do you think that the definition of Dijkstra's language is adequate
   for purposes of the paper?  What would have to be added for you to
   write a compiler for this language?  Do you think that a denotational
   or operational semantics would have served the paper as well?
q. (extra credit only; inside jokes about Dijkstra)
   Why doesn't this paper start with section 0?  Why are there two references
   to related work in the paper?  Can you find any extraneous words anywhere
   in the paper?  Why don't examples end with "(End of example.)"?