I M A G E B Y A N N A G A R M A T I Y

separately”) when writing assertions. For example, we might write:

 

as a specification of code that wires together two memory locations into a cyclic linked list. Here x  v says that pointer variable x holds the address of a memory location where v is stored (or more briefly, x points to v), and a command of the form [x] = v updates the location referred to by x so that its contents becomes v′.

The use of rather than the usual Bool-
ean conjunction ∧ ensures x and y are not
aliases—distinct names for the same lo-
cation—so that we have a two-element
cyclic list in the postcondition. A central
principle is that a command that mu-
tates a single location affects only one
*-conjunct: operational in-place update
is mirrored in the logic, addressing the
key difficulty where “an alteration to a
cell may affect the values of many syntac-
tically unrelated expressions.”
Reynolds was the first to describe a
program logic including the separating
conjunction; he defined an intuitionis-
tic (constructive) logic with *, 37 building
on earlier ideas of Burstall. 10 O’Hearn,
and Ishtiaq26 realized the assertion lan-
guage could be seen as an instance of the
resource logic BI of O’Hearn and Pym; 31
they independently discovered the same
intuitionistic logic as Reynolds, and
also saw that a more powerful Boolean
(nonconstructive) variant was possible
in which one could reason about explicit
memory management (Reynolds had as-
sumed garbage collection). They also in-
troduced the separating implication –*.