Algebraic separation logic

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.

Recommendations

Cites work

Cited in

(30)

Describes a project that uses

Uses Software

This page was built for publication: Algebraic separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q549676)