Lecture preparation

Assignment

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.