Topics for Final Exam in Com S 641 This test covers topics from homeworks 5-8. The final exam is Thursday, May 9, 2002, from 2:15-4:15pm in our usual room. REMINDERS This test is open book and notes. This test is timed. We will not grade your test if you try to take more than the time allowed. Therefore, before you begin, please take a moment to look over the entire test so that you can budget your time. For formal proofs, clarity and correct proof format are important. You can abbreviate steps as long as they are clear. READINGS Principally, chapters 7-9 and 11 of Back and von Wright's "Refinement Calculus: A Systematic Introduction", Springer-Verlag, 1998. See also chapters 2-3 of Edward Cohen's "Programming in the 1990s", Springer-Verlag, 1990, or my version of chapters 2-3 in the lecture notes, for more about predicate calculus. If you have more time, see the syllabus for further readings. TOPICS Topics marked + below are more important than topics marked - below. In general, things that are more like the homework will be more important, although I will feel free to ask some conceptual questions, especially those that integrate various topics. * Proofs (Back and von Wright chapter 6, Cohen chapters 2-3) + What constitutes a formally valid proof step in HOL? [HW5.1] + Give an counterexample for why a proof step is invalid. [HW5.1] - Prove properties about Boolean lattices using their inference rules [HW5.2-7] + Prove properties about the truth values, including quantifiers, using their inference rules [HW5.8-10] * Predicates and sets (Back and von Wright chapter 7) ** sets in HOL - How is set theory formalized in HOL? - How is the empty set represented in HOL? + Be able to translate statements involving sets into statements involving predicates. - Explain how this translation gives an ordering on sets that matches the usual ordering. + Prove properties of sets and predicates using the formal definitions of set operations in HOL. [HW5.11] + Be able to manipulate images and preimages of sets. - What is an indexed set? ** inference rules for complete lattices - What is a complete lattice? - Which lattices we have studied are complete? - What are the rules for reasoning about generalized join and meet? + Be able to use generalized join and meet in proofs. - What are the homomorphism properties of generalized join and meet (both on the range and on the index)? - How do these homomorphism properties relate to focusing rules? - How do the generalized join and meet of a complete lattice relate to quantifiers? ** selection and individuals - How does the selection operator embody the axiom of choice? + Use the selection operator in proofs. [HW5.12] - How is the arbitrary element constant defined? - What is the purpose of the type Ind and its infinity axiom? * Boolean expressions and conditionals (Back and von Wright chapter 8) ** Boolean expressions - Explain how terms are given a semantics using pointwise extension. + What is "reduction" and how is it used in proofs that involve Boolean terms? What is the purpose of it? + Prove properties of Boolean expressions. [HW6.1,3] ** conditionals - What are the useful inference rules for the conditional operator? - What focusing rules apply to the conditional operator? - How are conditional expressions defined? + Prove properties of conditional state transformers. [HW6.2] + Prove properties of conditional expressions. [HW6.4-5] * Relations (Back and von Wright chapter 9) ** fundamentals + How are relations modeled in HOL? + What alternative views of a relation are available for use in proofs? - How are relations ordered? + What lattice properties do relations have? - What are the top and bottom of the lattice of relations? - What do True and False correspond to in terms of programs? + What is the composition of relations? The inverse? - What is the state relation category? - What distributivity properties hold in the state relation category? + Prove properties of relations and their compositions. [HW7.1,7-8] ** coercion operators + How are predicates and functions coerced into relations? - What use are the coercion operators? + Be able to prove properties of coercions. - How are partial functions modeled using relations? ** relational assignment + What is a relational assignment? How does it generalize assignment? - How does a relational assignment model specification statements as in Morgan's book? + How are relational assignments best handled in proofs? ++ Prove properties of relational assignments. [HW7.2,6] ** reasoning and relations + Why do relations allow better modeling of programs than state transformations? (What properties do they model better?) + How are conditional state relations modeled? + How are guarded commands modeled? + Prove properties of conditional relations. [HW7.3] + How are loops modeled using relations? + What are the interpretations of refinement for state relations, and how do they relate to (a) contracts as games and (b) total vs. partial correctness? + How are specifications modeled using relational assignment? + Which interpretation of refinement is best suited to specifications? + Prove properties in the category of state relations. [HW7.4-5] ++ Prove properties about relational blocks. [HW7.9] * Predicate Transformers (Back and von Wright chapter 11) ** definitions + What are the weakest preconditions for the statements in the language of contracts? + What is a predicate transformer? + What is the refinement ordering on predicate transformers? + What are the lattice properties of predicate transformers? + How is composition defined on predicate transformers? Why is it that way? + What properties does composition of predicate transformers have? ++ Prove refinement or equivalence laws for contract statements. [HW8.1-4] ** basic predicate transformers + How are functional updates, assertions, and assumptions defined? + What are the weakest preconditions of abort, skip and magic? - What use is magic? + How are weakest preconditions of assignments calculated? ++ Calculate the weakest preconditions of straight-line programs. [HW8.6] ** relational updates + How are the two kinds of relational updates defined? - Why do these definitions correspond to the intuition given in chapter 1? + What are the weakest preconditions of chaos and choose? + What is the weakest precondition of a relational assignment? ++ Prove properties of the weakest preconditions of relational assignments. [HW8.7] + Calculate the weakest preconditions of programs that use conditionals. ** duality + How is the dual of a predicate transformer defined? - How is that like other notions of duality we studied? - How does duality relate to the interpretation of contracts as games in chapter 1? Why is this relationship correct? + Prove laws about duality of predicate transformers. [HW8.5] ** preconditions and guards - What are the miracle precondition and the abortion precondition? - What are the miracle guard and the abortion guard? - Which of these is most useful? - How do these relate to the theory of contracts as games? - How can the state space be partitioned using these?