6 - Separation algebras

Summary

Separation logics have assertions—for example P * (x ↦ y) * Q—that describe objects in some underlying model—for example “heaplets”—that separate in some way—such as “the heaplet satisfying P can join with (is disjoint from) the heaplet satisfying x ↦ y.” In this chapter we investigate the objects in the underlying models: what kinds of objects will we have, and what does it mean for them to join?

This study of join relations is the study of separation algebras. Once we know how the underlying objects join, this will explain the meaning of the * operator (and other operators), and will justify the reasoning rules for these operators.

In a typical separation logic, the state has a stack ρ for local variables and a heap m for pointers and arrays. Typically, m is a partial function from addresses to values. The key idea in separation logic is that that each assertion characterizes the domain of this function as well as the value of the function. The separating conjunction P * Q requires that P and Q operate on subheaps with disjoint domains.

In contrast, for the stack we do not often worry about separation: we may assume that both P and Q operate on the entirety of the stack ρ.

For now, let us ignore stacks ρ, and let us assume that assertions P are just predicates on heaps, so m ⊨ P is simply P(m).