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.

[edit] and

is the dual/adjoint of

implies that

[edit] References

• Separation Logic: A Logic for Shared Mutable Data Structures - The most cited separational logic introduction paper on LICS'02.
• Information on Local Reasoning and Separation Logic
• Introduction to Separation Logic