Separation Logic (SL)

SL consists of all the connective and quantifiers from classical logic, plus two new connectives: a separating conjunction (PQP*Q) and a separating implication PQP{-*}Q.

Semantic domains:

Locations: L\mathbb{L}
Addressable locations: A=L{null}\mathbb{A} = \mathbb{L} \setminus \{ null\}
Integers: Z\mathbb{Z}
Values: V=LZ\mathbb{V} = \mathbb{L} \cup \mathbb{Z}
Variables: Var\mathcal{Var}
Stacks: S=VarVS = \mathcal{Var} \rightarrow \mathbb{V}
Heaps: H=LfVH = \mathbb{L} \rightarrow_f \mathbb{V}

A set of location, denoted by L\mathbb{L}, which is ordered and disjoint from the set of integers Z.\mathbb{Z}.
Var\mathcal{Var} contains program variables and logical variables.

Stacks maps variables to values.
Heaps maps locations to values.
Since we wish to track allocation, the heap is a partial function whose domain consists of only those locations that have been allocated. Thus, the domain of heaps is the set of partial functions from locations to values.

The models consist of pairs from S×HS\times H.

Separation logic syntax

Variables x,yx,y \in Var\mathcal{Var}
Integers nn \in Z\mathbb{Z}
Integer Exp ii ::=::= $ n\mid\ x\mid\ i_1+i_2\mid\ i_1-i_2\mid\ i_1\times i_2 $
Pointer exp kk ::=::= x x.n nullx\mid\ x.n\mid\ null
Boolean exp bb ::=::= i1=i2 k1=k2i_1=i_2\mid\ k_1=k_2
$i_1<i_2\mid\ \neg P \mid\ P_1 \land P_2\mid\ $
P1P2  P_1 \lor P_2\mid\ \bot\mid\ \top
Expression ee ::=::= i b ki\mid\ b\mid\ k
Heap predicates Σ\Sigma hh ::=::= k \mapsto e \mid\ \textbf{emp}
Pure formula Π\Pi p,qp,q ::=::= $b\mid\ p\land q \mid\ p\lor q\mid\ p \Rightarrow q\mid\ \neg p\mid\ $
pq pq x.p x.pp * q \mid\ p{-*}q \mid\ \forall x.p\mid\ \exists x.p
Formulas ϕ,ψ\phi,\psi ::=::= b h ϕψ ϕψb\mid\ h\mid\ \phi \land \psi\mid\ \phi \lor \psi
$\phi \Rightarrow \psi \mid\ \neg \phi \mid\ \phi * \psi \mid\ \phi {-*} \psi\mid\ $
$\forall x.\phi \mid\ \exists x.\phi $

The locations are ordered. x.nx.n stands for the nthn^{th} location after xx in this ordering. nullnull is the non-addressable element of L\mathbb{L}.

The heap predicate \textbf{emp} states that the heap is empty (its domain is the empty set).

The predicate EFE \mapsto F indicates that the heap contains a single cell at location EE, which contains the value given by FF.

Heaps with more than one cell are represented by combining these predicates with *. The formula pqp*q holds if the heap can be split into two disjoint parts, one of which satisfies pp while the other satisfies qq.

There is a special syntactic class of pure formulas, which are those formulas that do not contain heap predicates.

To prove Π1Σ1Π2Σ2\Pi_1 \land \Sigma_1 \Rightarrow \Pi_2 \land \Sigma_2, it is sufficient to show that Π1Π2\Pi_1 \Rightarrow \Pi_2 and Σ1Σ2\Sigma_1 \Rightarrow \Sigma_2.

Π1Π2\Pi_1 \Rightarrow \Pi_2 is settled by standard classical logic theorem prover, such as Simplify or Vampyre.

Smallfoot was the first implementation to use separation logic, its goal to verify the extent to which proofs and specifications made by hand could be treated automatically [BCO05]. The automatic part is related to the assertion checking, but the user has to provide preconditions, postconditions, and loop invariants.

Besides, as for modal and temporal logics, the relationships between separation logic, and first-order or second-order logics have been the source of many characterizations and works. This is particularly true since the separating connectives are secondorder in nature, see e.g. [Loz04a, KR04, CGH05, BDL12]. For instance, separation logic is equivalent to a Boolean propositional logic [Loz04b, Loz04a] if first-order quantifiers are disabled. Similarly, the complexity of satisfiability and model-checking problems for separation logic fragments have been quite studied [COY01, Rey02, CHO+11, AGH+14, BFGN14]. In [COY01], the model-checking and satisfiability problems for propositional separation logic are shown PSPACE-complete; this is done by proving a small model property.