Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

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 and Generalizing Abstraction Functions by Butler Lampson.

Why are we reading these handouts?

What to learn from these handouts?

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.