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.