This paper tackles three problems:
Supporting user-defined predicates in separation logic, adding OPEN and CLOSE rules to unfold and fold their definitions.
Placing restrictions on where OPEN/CLOSE can be used in order to enforce data abstractions.
Generalizing abstract predicates to support object-oriented languages by adding abstract predicate families that can be indexed by the class.
There are a number of examples manually proved in this paper.
Papers related to Separation logic and abstraction
- Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]