Heap Monotonic Typestate
- Manuel Fahndrich ,
- Rustan Leino
Proceedings of the first International Workshop on Alias Confinement and Ownership (IWACO) |
The paper defines the class of heap monotonic typestates. The monotonicity of such typestates enables sound checking algorithms without the need for non-aliasing regimes of pointers. The basic idea is that data structures evolve over time in a manner that only makes their representation invariants grow stronger, never weaker. This assumption guarantees that existing object references with particular typestates remain valid in all program futures, while still allowing objects to attain new stronger typestates. The system is powerful enough to establish properties of circular data structures.