Questions: Separation Logic

Question 1

What does the separating conjunction P * Q assert about the heap?

• A. P and Q both hold for the entire heap
• B. The heap can be divided into two disjoint regions, one satisfying P and the other satisfying Q
• C. Either P or Q holds for the heap, but not both
• D. P holds for the heap and Q holds for the stack

Answer: (B)

The separating conjunction P * Q requires the heap to split into two parts with NO shared cells — one part satisfies P, the other satisfies Q. This disjointness is what distinguishes it from ordinary conjunction (P and Q, which says both hold for the same heap) and enables reasoning about ownership and aliasing. If x points to 5 in one part and y points to 7 in the other, the * guarantees x and y are different addresses.

Question 2

The frame rule in separation logic states: if {P} C {Q} then {P * R} C {Q * R}, provided C does not modify variables free in R. Why is this rule central to scalability?

Model answer: The frame rule enables local reasoning: you prove a specification for C that mentions only the heap cells C actually accesses (the footprint). The frame R represents the rest of the heap, which is automatically preserved. This means you can verify each function in isolation against its small footprint, then compose proofs without re-verifying the entire heap — making verification modular and scalable to large programs.

Without the frame rule, every specification would need to describe the entire heap, and adding a new data structure would require re-proving every existing function. The frame rule's guarantee that untouched heap is preserved is what makes separation logic practical for real codebases. Tools like Facebook's Infer use this principle to analyze millions of lines of code by reasoning locally about each function.

Question 3

Standard Hoare logic cannot easily handle pointer aliasing (two variables pointing to the same memory cell). How does separation logic address this?

Model answer: The separating conjunction x -> v * y -> w inherently asserts that x and y point to different cells (disjoint heap regions). This makes non-aliasing the default in separation logic specifications. When aliasing IS intended, it must be expressed explicitly, typically by using a single points-to assertion x -> v and noting that y = x. This reversal of defaults — non-aliasing unless stated otherwise — eliminates the combinatorial explosion of aliasing cases that plagues standard Hoare logic.

In standard Hoare logic, if you have two pointers x and y, you must consider whether they alias (point to the same cell) or not, and proofs branch on every such possibility. With n pointers, this creates 2^(n choose 2) cases. Separation logic's * operator makes disjointness structural: x -> v * y -> w cannot be satisfied if x = y because the heap regions must be disjoint. This eliminates aliasing cases from proofs entirely unless aliasing is explicitly introduced.