Separation logic

Separation Logic, a term attributed to John C. Reynolds, is an extension of Hoare logic that describes variations on program logic in computer science.

In particular, 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); and
* virtual separation (modular reasoning) between concurrent modules.

Separation Logic supports the developing field of research described by Peter O'Hearn and Hongseok Yang as "local reasoning".

$ast$ and $-ast$

$-ast$ is the dual/adjoint of $ast$

$S,\; H\; models\; P\; -ast\; Q\; Longleftrightarrow\; forall\; H\text{'}.(S,\; H\text{'}\; models\; P$ implies that $S,\; H\; ast\; H\text{'}\; models\; Q)$

References

* [http://citeseer.ist.psu.edu/reynolds02separation.html Separation Logic: A Logic for Shared Mutable Data Structures] - The most cited separational logic introduction paper on LICS'02.
* [http://www.dcs.qmul.ac.uk/~ohearn/localreasoning.html Information on Local Reasoning and Separation Logic]
* [http://www.cl.cam.ac.uk/~mjp41/IntroSep.pdf Introduction to Separation Logic]