Separation logic, an extension of Hoare logic, is currently a very active area of research. This paper investigates the expressiveness of this logic by exploring various restricted forms of it. Relations between fragments of separation logic and related logics are also studied, and via translations the relationships between these logics are expressed.
The introduction of the paper explains known results, describes the results that are derived in the following sections, and gives a map showing the relationships between the various logics.
The following sections introduce some restricted form of separation logic where formulas contain only one record field and a finite number of bounded variables. Next, some formulas often used in the following sections are defined and an encoding of data words via these formulas is presented. The kind of heaps used in this encoding, called fishbone heaps, are used a lot throughout the remainder of the paper. Finally, the section is concluded by the presentation of a new special variant modal logic for describing heaps. Section 3 builds on the previous section by further advancing the technical terms and constructing a translation from the propositional temporal interval logic into separation logic with two quantified variables and without the so-called “magic wand” operator. The possibility of this translation yields that separation logic with two quantified variables is decidable but not elementary recursive. The fourth section finally proves that the satisfiability problem of the separation logic with two bounded variables and the “magic wand” operator is not decidable. This is achieved by encoding Minsky machines and reducing the halting problem. A conclusion wraps up the results and points out some research directions.
The paper contains a lot of technical tricks, which are nevertheless presented in a way that is very intuitively graspable. The intuition of fishbone heaps and the depiction of their structure are very helpful. On the whole, I consider this a very enjoyable paper.
