Differences between revisions 9 and 10
⇤ ← Revision 9 as of 2011-02-03 21:06:00 →
Size: 2536
Editor: viktor
Comment:
← Revision 10 as of 2011-02-03 21:16:16 → ⇥
Size: 2450
Editor: viktor
Comment:
Deletions are marked like this. Additions are marked like this.
Line 3: Line 3:
Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system. Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for ''local reasoning'', where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.
Line 7: Line 7:
'''Proof rules.''' SL inherits the standard rules and axioms of Hoare logic, has its own proof rules for heap-manipulating commands, and the all-important frame rule. ==== The frame rule ====
Line 11: Line 11:
This says that a program that runs correctly with a heap satifying its precondition also runs correctly with a bigger initial heap. Further, it is guaranteed not to touch the additional portion heap.

The frame rule enables ''local reasoning'': the specification of a program need only mention the portion of the heap used by the program.		 The frame rule is the crux of ''local reasoning''. It says that a program that runs correctly with a heap satisfying the precondition, <<latex($P$)>>, also runs correctly with a bigger initial heap, <<latex($P * F$)>>. Further, the program is guaranteed not to touch the additional portion of heap, and so <<latex($F$)>> remains true in the postcondition. Therefore, programs specifications need only describe the ''footprint'' of the program (i.e., the part of the heap it accesses). Using the frame rule, these specifications can be applied in any larger context.
Line 19: Line 17:
=== Extensions of Separation Logic === === Extensions & tool support ===
Line 21: Line 19:
There are extensions of separation logic: There are numerous extensions of separation logic for better handling:
Line 28: Line 26:
=== Tool support ===

Separation logic has also been extensively used in semi-automatic and automatic program analyses (often known as shape analyses) for proving functional correctness of programs or simply the absence of certain kinds of runtime errors and/or memory leaks.

For more information, see [[ToolSupport]].		 There are also many SL-based tools such as entailment provers and static analyzers. For more information, see [[ToolSupport]].

Separation logic

Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.

Assertions. Separation logic assertions describe heaps. Besides the normal logical connectives (conjunction, disjunction, implication, etc), SL introduces the separating conjunction ($*$) of two assertions. A heap satisfies the separating conjunction of two assertions if it can be divided into two disjoint parts satisfying the two assertions. Formally, $h \models P_1 * P_2$ if and only if there exist (disjoint) $h_1$ and $h_2$ such that $h = h_1 \uplus h_2$ and $h_1 \models P_1$ and $h_2 \models P_2$.

The frame rule

$$\frac{ \{P\}~C\{Q\} }{ \{P*F\}~C\{Q*F\} }\quad \mathbf{fv}(F)\cap\mathbf{mod}(C) = \emptyset$$

The frame rule is the crux of local reasoning. It says that a program that runs correctly with a heap satisfying the precondition, $P$, also runs correctly with a bigger initial heap, $P * F$. Further, the program is guaranteed not to touch the additional portion of heap, and so $F$ remains true in the postcondition. Therefore, programs specifications need only describe the footprint of the program (i.e., the part of the heap it accesses). Using the frame rule, these specifications can be applied in any larger context.

Introductory material

Extensions & tool support

There are numerous extensions of separation logic for better handling:

  • Abstraction (hypothetical frame rule, abstract predicates, context logic)

  • Concurrency (CSL, locks-in-the-heap, RGSep/SAGL/LRG, deny-guarantee)

  • Assembly code
  • Higher-order functions

There are also many SL-based tools such as entailment provers and static analyzers. For more information, see ToolSupport.

Further reading

TODO

SeparationLogic (last edited 2011-02-07 13:18:06 by viktor)