- Pointer aliasing can break encapsulation and invalidate data structure invariants.
- Representation independence (RI) is nontrivial to guarantee in a generic manner, without recourse to specialized disciplines such as ownership.
- Mechanical verification of RI using theorem provers is nontrivial because it requires relational reasoning between two different data structure representations. Such reasoning lies outside the scope of most modern verification tools.
We address the challenge by reasoning in Region Logic (RL), a Hoare logic augmented with state dependent “modifies” specifications based on simple notations for object sets, termed "regions". RL uses ordinary first order logic assertions to support local reasoning and also the hiding of invariants on encapsulated state, in ways suited to verification using SMT solvers. By using relational assertions, the logic can reason about behavior-preservation of data structure refactorings even in settings where full functional pre/post specifications are absent. The key ingredient behind such reasoning is a new proof rule that embodies representation independence.
This work is in collaboration with David A. Naumann and Mohammad Nikouei (Stevens Institute of Technology).
