Comparing Heap Models: Ownership, Dynamic Frames, Permissions
- Rustan Leino
Typing, Analysis and Verification of Heap-Manipulating Programs, Dagstuhl, Germany |
Published by Microsoft Research
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