Topics for Exam 1 in Com S 641

This test covers topics from homeworks 1-4, and the first part of
homework 5.

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 syntax are important.

READINGS

Principally, chapters 1-6 of Back and von Wright's "Refinement
Calculus:  A Systematic Introduction", Springer-Verlag, 1998.

See chapters 1-6 (especially 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.  (For example,
I might ask: "Is the refinement ordering on contracts a bounded lattice?)

* introduction
    - what are the three kinds of semantics and what do they tell you
      about a statement?
    - what is the difference between a model and a theory, and how do
      they relate?  What is a model of HOL?

* overview (Chapter 1)
    - What is a state?  A state space?  What are the operations on states?
    - How is state update modeled?
    - What's the purpose of a contract?
    - What does ";" mean for contracts?  What does \join mean?
    - When are two contracts equal?
    - What is an agent? What does it mean for two agents to interact?
    - What's the meaning of an assertion?  How does it differ from an
      assumption?   How do these relate to pre- and postconditions?
    - What does it mean to satisfy a contract?  To breach it?
    - Explain the duality between our agent's actions and the other agent's.
    - Which side are the angels on?  The demons?
    - What does it mean if the angels have a winning strategy?
    - How can a demon lose?
    - How is nontermination handled?
    + What does refinement mean for contracts?
    - Which is better?
    + Is refinement a partial order on contracts?  A lattice?
      Bounded? Complete?
    - How would you define abort? skip?
    - What kinds of contracts are best used as specifications?
    - What is a relational assignment?  How is it useful as a specification?
    - How is a pre- and postcondition specification of a procedure  modeled?
    - What does it mean for a statement to be correct?

* posets-lattices-categories (Chapter 2)
    + Understand definitions of properties of posets and lattices [HW1.2-3]
    - What is a congruence?
    + Give examples of posets, their orders, and meet and join
      operations.  (Esp. for the integers, sets, and booleans.)
    + Draw and read Hasse diagrams for posets [HW1.1]
    + What's the difference between a monotonic function and an order
      embedding? 
    - If a poset has a top element is it a lattice?
    - If a poset has a bottom element, do meets exist in it?
    - If a poset is bounded, is it a lattice?
    - What is a complete lattice?
    - If a lattice has a bottom and a top element, is it complete?
    - What is a Boolean lattice, and how does it differ from a
      complete lattice?
    - What is an atomic lattice?
    - What is the dual of a lattice?
    - Explain pointwise extension for products and function spaces.
    - How do the ordering properties of the function space A -> B
      relate to the properties of A and B?
    - What is homomorphism?
    - How do the homomorphism properties relate to each other and to
      monotonicity? 
    ++ Write calculational-style proofs of various properties of posets and
      lattices [HW1.4-11]
    - What is a category?  Give some examples.
    - What is a functor?  Give examples.
    - In what sense does a category generalize the kinds of properties
      we have studied so far?

* higher-order-logic (Chapter 3)
    + Give types of terms in HOL [HW1.12-13]
    - What is a type structure?
    - What is a model of HOL?  How does it give meaning to terms?
    - How do the properties of a standard model relate to the axioms about
      truth values in HOL?
    - What is a sequent?  An inference?
    + When is an inference valid in HOL?
    + What is needed to have a counterexample to an inference's validity?
    - Write derivations based on inference rules [HW1.14]
    - Explain how to deal with subtyping in HOL [HW1.15]
    - What is soundness and completeness for a theory?
    - What is consistency important?    

* functions (Chapter 4)
    + Be able to reason about equality in HOL
    + What's the meaning of "t1 is free for v in t"?
    - Derive inference rules from other inference rules in HOL [HW2.1-3]
    + Be able to use the lambda calculus rules (alpha, beta, eta,
      extensionality) to reason about functions in HOL.
    + Prove properties using definitions and local definitions in HOL [HW2.4-6]
    - Prove properties about products in HOL

* states-and-state-transformers (Chapter 5)
    - What is a state space?  A state transformer?
    - What is a variable in the semantics?  How is it modeled?
    - What do the axioms for attributes mean?
    - How are expressions modeled?  What overloadings are used?
    - How is assignment modeled?
    - What does simultaneous assignment do?  What does x,y := (y+1),(x+1) do?
    - What does "var x:T" mean?
    - How are local blocks modeled?
    - What is the substitution property?
    ++ Prove properties of state transformers using the independence
    assumptions [HW3.1]
    ++ Prove properties of straight-line programs [HW3.2-5]
    + Prove properties of procedure definitions, using both call by
    reference and call by value [HW3.6]

* truth-values (Chapter 6)
    + How do the inference rules for the truth values relate to the
      inference rules for Boolean lattices?
    - What properties of the truth values are special (that are not
      true about Boolean lattices in general?
    + How do inference rules relate to the calculational proof format?
      (For example, where do the hypotheses go?)
    + What shapes of calculational proofs are valid for proving a
      formula t?  (I.e., what can a proof of |- t look like?)
    + How do you use case analysis in a proof?
    - Why are the side conditions important in the quantifier rules?
    + Prove properties about Boolean lattices using their inference
      rules [HW4.1]
    ++ Prove properties about the truth values, including quantifiers,
      using their inference rules [HW4.2-7]