Before lecture, read the paper assigned below, and submit two items
to the submission website
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Read the handouts on
Abstraction Functions and Invariants
Generalizing Abstraction Functions
by Butler Lampson.
Why are we reading these handouts?
The handouts describe the ideas of refinement, invariants, and
abstraction functions. These ideas are widely used in verification,
but most of the other papers we read take them for granted.
What to learn from these handouts?
How to think of specifications and correctness in terms of
refinement, invariants, and abstractions.
When are abstraction relations necessary?
Answer this question
Why does it not always work to define an abstraction function from code state
to spec state in order to do a simulation proof that the code implements the
spec? Assuming that the spec doesn’t make any premature decisions, what are two
ways to extend the abstraction function idea so that it will always work?
The section in handout 6 labeled "Abstraction functions and simulation" and
pages 4-6 in handout 8 are the most relevant.