Separation Logic is a sub-structural logic that supports local
reasoning for imperative programs. It is designed to elegantly
describe sharing and aliasing properties of heap structures, thus
facilitating the verification of programs with pointers.
In past work, separation logic has been developed for heaps containing records of basic data types.
Languages like C or ML, however, also permit the use of code
pointers. The corresponding heap model is commonly referred to as
higher-order store since heaps may contain commands which in
turn are interpreted as partial functions between heaps.
In this paper we make Separation Logic and the benefits of local reasoning available to languages with higher-order store. In particular, we introduce an extension of the logic and prove it sound, including the Frame Rule that enables specifications of code to be extended by invariants on parts of the heap that are not accessed.
Download PDF Show BibTeX
Login to edit