Algebraic separation logic (Q549676)

Separation logic is an extension of Hoare logic with reasoning about complex and shared data structures by added assertions to express separation between memory regions. For arbitrary assertions \( p\) and \(q\) the conjunction \(p \star q\) asserts that \(p\) and \(q\) both hold, but each for separate parts of the storage, and \(p-\star q\) holds for a region if (roughly) \(p\) holds in another region then \(q\) holds in joint region of these two regions. In this paper an algebraic approach to separation logic is presented. In particular, an algebraic characterization for assertions of separation logic is given and different classes of assertions are discussed. A relational semantics of the commands of a simple programming language associated with separation logic is given by the presented algebraic framework. It is shown how to algebraically formulate the requirement that a command preserves certain variables. It is claimed that the algebraic view does not only yield new insights into separation logic but also shortens proofs due to a point-free representation.