Abstract

Specification challenges

  • Invariants
    • Describes what holds of an object in its steady state
    • When does an invariant hold?
  • Frames
    • Describes what is being modified or read
  • Goals
    • Flexibility
    • Conciseness