> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/logic-types/separation-logic.md). # Separation logic Separation logic is an extension of [Hoare logic](/math-debrief/300-logic/logic-types/separation-logic.md), a way of reasoning about programs. The assertion language of separation logic is a special case of the [logic of bunched implications](/math-debrief/300-logic/logic-types/bunched-logic.md) (BI). Separation logic facilitates reasoning about: * programs that manipulate pointer data structures—including information hiding in the presence of pointers * "transfer of ownership" (avoidance of semantic frame axioms) * virtual separation (modular reasoning) between concurrent modules Separation logic supports the developing field of research described by Peter O'Hearn and others as *local reasoning*, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include *automated parallelization of software*, and *automated program verification*, where an algorithm checks the validity of another algorithm. Separation logic assertions describe states consisting of a store and a heap, roughly corresponding to the state of local, stack-allocated, variables and dynamically-allocated objects. A store s is a function mapping variables to values. A heap ℎ is a partial function mapping memory addresses to values. Two heaps ℎ and ℎ′ are disjoint, denoted ℎ ⊥ ℎ′, if their domains do not overlap; i.e. for every memory address ℓ, at least one of ℎ(ℓ) and ℎ′(ℓ) is undefined. The logic allows to prove judgements of the form s,ℎ ⊨ P, where s is a store, ℎ is a heap, and P is an assertion over the given store and heap. Separation logic assertions (denoted as P, Q, R) contain the standard boolean connectives and, in addition, `emp`, e ↦ e', P ∗ Q, and P −∗ Q, where e and e′ are expressions. The constant `emp` asserts that the heap is empty, i.e. s,ℎ ⊨ emp when ℎ is undefined for all addresses. The binary operator ↦ takes an address and a value and asserts that the heap is defined at exactly one location, mapping the given address to the given value. s,ℎ ⊨ e ↦ e′ when ℎ $${\displaystyle h(\[!\[e]!]*{s})=\[!\[e']!]*{s}}$$,\ where $${\displaystyle \[!\[e]!]\_{s}}$$ denotes the value of expression e evaluated in store s, and ℎ is otherwise undefined. The binary operator ∗ ($$\ast$$)\ (pronounced star or separating conjunction) asserts that the heap can be split into two disjoint parts where its two arguments hold, respectively. s,ℎ ⊨ P ∗ Q when there exist $${\displaystyle h\_{1},h\_{2}}$$ such that\ $${\displaystyle h\_{1},\bot ,h\_{2}}$$ and $${\displaystyle h=h\_{1}\cup h\_{2}}$$ and $${\displaystyle s,h\_{1}\models P}$$ and $${\displaystyle s,h\_{2}\models Q}$$ The binary operator −∗\ (pronounced magic wand or separating implication) asserts that extending the heap with a disjoint part that satisfies its first argument results in a heap that satisfies its second argument. $${\displaystyle s,h\models P-!!\ast ,Q}$$\ when for every heap $${\displaystyle h',\bot ,h}$$ such that $${\displaystyle s,h'\models P}$$, also $${\displaystyle s,h\cup h'\models Q}$$ holds.