Com S 641 Semantic Models for Programming Languages Homework: 0 This homework is to help guide your reading of the paper by Hoare that we'll discuss in the next class meeting (or so). C.A.R. Hoare. An Axiomatic Basis for Computer Programming, CACM, 10(12):576-580,583, 1969. (Section 2) a. Are there any axioms besides those in Table I that are true of both the infinite set of all "nonnegative integers" (the naturals) and finite sets of integers in the three interpretations of Table II? If so, give one or more examples. (Are such example axioms "interesting"?) b. Why does Hoare insist on treating only "nonnegative integers"? How would you expand his treatment to consider negative integers also? (Section 3) Note that Hoare's notation P {Q} R would nowdays be written {P} Q {R} to emphasize the role of the assertions P and R as comments (as in Pascal). c. Why is it the case that a specification "will usually not ascribe particular values to variables, but will rather specify certain general properties"? Can you give an example? d. The focus on variables may be a limitation of Hoare's approach. Is it reasonable to think of the input and output of a whole program as a variable? Is there any reasonable way to extend Hoare's approach to deal with pure functional languages? e. (Section 3.1) What do you think about the following objection to the assignment axiom schema: the axiom is incorrect, because the expression f is, on the one hand, written in the programming language, and on the other hand used as part of the formula P ? 0 f. Is the limitation to side-effect free expressions a good idea? What do you think of Hoare's claim in the first paragraph of section 4? Do you think it possible to eliminate side-effects from the expressions in a programming language? (How about in an OO programming language?) If so, how could a programming language help the programmer/verifier to prove the absence of side-effects in expressions? Would the restriction of no side-effects in expressions be something you could live with in your own programming? g. (Section 3.2) The footnote at the bottom of page 577 says that the turnstile ( |- ) means theoremhood. Does this mean theoremhood only in the system being presented here? What does the formula |- R ) S mean in the rules of consequence? h. (Section 3.3) What's another name for the simplifications described in the first paragraph of section 3.3? Do you think that the writing would be improved by naming it? Or by just assuming it? i. Does the formal rule (D2) help make what Hoare is saying clearer? (Compare the previous paragraph with the formal rule.) j. (Section 3.4) Do you think that there is anything that the rule of iteration (D3) would not be able to prove? If you think so, give an example. k. Is the following a valid deduction? Why or why not? true { while 3 < 4 do x := x + 1 } 3 = 4 What does that mean? l. (Section 3.5) Hoare says that the proof in Table III is "excessively tedious". To what extent does the proof in Table III reflect your way of thinking about the correctness of the program? Give an abstraction of the proof that combines steps, so that it less tedious, but still seems rigorous. m. (extra credit; meaning you don't have to do this...) Does the specification given for the program proved in Table III really capture everything assumed in the proof? n. (extra credit; meaning you don't have to do this...) Can prove any lemmas that would reduce the tedium of the proof in Table III while maintaining rigor? Are there any rules of thumb for such proofs? (Section 4) o. What do you think of Hoare's remarks about termination? Do you think his idea a fruitful instance of separation of concerns or a fundamental flaw? (Section 5) p. Do you think that "the practical advantages of program proving will outweigh the difficulties" and the costs of testing, debugging, and removing errors after the program is finished? (extra credit: find for some literature on such cost tradeoffs.) q. Do you think that Hoare's proof technique is a practical way to document programs? To ensure that programs are machine independent? (Section 6) Historically, Hoare's paper is nearly contemporary with the development of denotational semantics (Strachey's work first started being published in 1966), follows closely on the first formal operational semantics (McCarthy's in 1960, which has circularity problems), and just follows Landin's work on operational semantics (1964). All of this work closely followed the publication of the Algol 60 report and its revision, which introduced formal notation for syntax. r. What language design principle would you draw from Hoare's discussion in this section? For example, what does Hoare advocate that you avoid in designing a programming language? Do you think, given the limitations of Hoare's work (see section 4), that this is a good idea? Why? s. (extra credit only) Hoare claims that axioms can be stated independently of each other, thus making a language description orthogonal. Consider what would happen if one had side-effects in expressions, aliasing, or continuations in a language. Would the other axioms be unaffected by this? (doctoral thesis: if not, design an axiomatic framework that has such a desirable property) (General questions) t. How would you summarize the contribution of this paper in a few sentences? u. (extra credit only) What does Hoare's system have to do with "structured programming", if anything? v. (extra credit only) The post-conditions in a Hoare triple (i.e., R in P{Q}R) are predicates on only a single state. In Z, VDM, Larch/C++, and other specification languages, post-conditions are predicates on two states. Is this a problem for Hoare logic? Is there a logical trick that can get around it? w. (extra credit only) In standard logic, one can prove an implication by proving its contrapositive. Can this be done in Hoare logic? Is that a problem? x. (extra credit only) In a Hoare triple, P{C}Q, the predicates P and Q live in a different world than the command C. Before reading the Dijkstra paper, think about whether there is any fruitful way to combine the two worlds, so that, for example, you could do something like conjoining two Hoare triples to from another Hoare triple, etc. y. (extra credit only) Does Hoare logic give any help in reasoning about parallel programs? What about nondeterministic programs?