# Separation Logic

## Separation Logic (SL)

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

### Semantic domains:

Locations: $\mathbb{L}$

Addressable locations: $\mathbb{A} = \mathbb{L} \setminus \{ null\}$

Integers: $\mathbb{Z}$

Values: $\mathbb{V} = \mathbb{L} \cup \mathbb{Z}$

Variables: $\mathcal{Var}$

Stacks: $S = \mathcal{Var} \rightarrow \mathbb{V}$

Heaps: $H = \mathbb{L} \rightarrow_f \mathbb{V}$

A set of location, denoted by $\mathbb{L}$, which is ordered and disjoint from the set of integers $\mathbb{Z}.$

$\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\times H$.

### Separation logic syntax

Variables | $x,y$ | $\in$ | $\mathcal{Var}$ |

Integers | $n$ | $\in$ | $\mathbb{Z}$ |

Integer Exp | $i$ | $::=$ | $ n\mid\ x\mid\ i_1+i_2\mid\ i_1-i_2\mid\ i_1\times i_2 $ |

Pointer exp | $k$ | $::=$ | $x\mid\ x.n\mid\ null$ |

Boolean exp | $b$ | $::=$ | $i_1=i_2\mid\ k_1=k_2$ |

$i_1<i_2\mid\ \neg P \mid\ P_1 \land P_2\mid\ $ | |||

$P_1 \lor P_2\mid\ \bot\mid\ \top$ | |||

Expression | $e$ | $::=$ | $i\mid\ b\mid\ k$ |

Heap predicates $\Sigma$ | $h$ | $::=$ | k \mapsto e \mid\ \textbf{emp} |

Pure formula $\Pi$ | $p,q$ | $::=$ | $b\mid\ p\land q \mid\ p\lor q\mid\ p \Rightarrow q\mid\ \neg p\mid\ $ |

$p * q \mid\ p{-*}q \mid\ \forall x.p\mid\ \exists x.p$ | |||

Formulas | $\phi,\psi$ | $::=$ | $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.n$ stands for the $n^{th}$ location after $x$ in this ordering. $null$ is the non-addressable element of $\mathbb{L}$.

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

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

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

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

To prove $\Pi_1 \land \Sigma_1 \Rightarrow \Pi_2 \land \Sigma_2$, it is sufficient to show that $\Pi_1 \Rightarrow \Pi_2$ and $\Sigma_1 \Rightarrow \Sigma_2$.

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

## related work

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.