Separation logic
From Wikipedia, the free encyclopedia
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.
