Separation Logic - Revision history

Ajreynol at 16:59, 2 August 2018

2018-08-02T16:59:34Z

2016-11-29T15:54:34Z

2016-11-28T21:11:53Z

2016-11-28T21:09:48Z

2016-11-28T20:37:32Z

2016-11-28T20:37:12Z

2016-11-28T20:35:59Z

2016-11-28T20:34:06Z

2016-11-28T20:33:49Z

2016-11-28T20:30:44Z

@@ Line 58: / Line 58: @@
 | Empty heap
 | <code>N/A</code>
-| <code>('''emp''' X Y)</code>
+| <code>(_ '''emp''' T1 T2)</code>
-| <code>em.mkExpr('''kind::SEP_EMP''', X, Y);</code>
+| <code>em.mkExpr('''kind::SEP_EMP''', X, Y);</code> where X and Y are of type T1 and T2.
 |-
 | Points-to
@@ Line 100: / Line 100: @@
    (declare-const x U)
    (declare-const a Int)
-   (assert (and (not (emp x 0)) (pto x a))
+   (assert (and (not (_ emp Int U)) (pto x a))
    (check-sat)

@@ Line 3: / Line 3: @@
 =Signature=
-Given a (decidable) base theory T, CVC4 supports a [http://homepage.divms.uiowa.edu/~ajreynol/atva16.pdf decision procedure] for <math>SL(T)_{Loc,Data}</math> formulas, where "Loc" and "Data" are any sort belonging to T.
+Given a (decidable) base theory T, CVC4 has a [http://homepage.divms.uiowa.edu/~ajreynol/atva16.pdf decision procedure] for quantifier-free <math>SL(T)_{Loc,Data}</math> formulas, where "Loc" and "Data" are any sort belonging to T.
 A <math>SL(T)_{Loc,Data}</math> formula is one from the following grammar:
    F : L | (emp t u) | (pto t u) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op ... op Fn

@@ Line 12: / Line 12: @@
 =Semantics=
-A satisfiability relation <math>I,h \models_{SL} \varphi</math> is defined for <math>SL(T)_{Loc,Data}</math> formulas,
+A satisfiability relation <math>I,h \models_{SL} \varphi</math> is defined for <math>SL(T)_{Loc,Data}</math> formulas <math>\varphi</math>,
 where I is an interpretation, and h is a heap. The semantics of separation logic operators are as follows:
@@ Line 40: / Line 40: @@
 where <math>h_1 \uplus \ldots \uplus h_n</math> denotes the disjoint union of heaps <math>h_1, \ldots, h_n</math> and
 <math>h'\#h</math> denotes that heaps h' and h are disjoint, and <math>nil</math> is a distinguished variable of sort Loc.
-Notice that the arguments of "emp" are used to denote the type of the heap and have no meaning otherwise.
+All classical Boolean connectives are interpreted as expected.
 =Syntax=

@@ Line 91: / Line 91: @@
    (assert (and (pto x a) (pto x b)))
    (assert (not (= a b)))
    (check-sat)

@@ Line 1: / Line 1: @@
 CVC4 supports a syntax for separation logic as an extension of the *.smt2 language.
-=Signature and semantics=
+=Signature=
 Given a (decidable) base theory T, CVC4 supports a [http://homepage.divms.uiowa.edu/~ajreynol/atva16.pdf decision procedure] for <math>SL(T)_{Loc,Data}</math> formulas, where "Loc" and "Data" are any sort belonging to T.

@@ Line 105: / Line 105: @@
 Given a separation logic input,
 the sorts Loc and Data are inferred by CVC4, and must be consistent across all predicates occurring in an input.  CVC4 does not accept an input such as:
    (declare-sort U 0)
    (declare-const x U)
    (assert (and (pto x 0) (pto 1 2)))
 since the sorts of the first arguments of the points-to predicates do not agree.

@@ Line 9: / Line 9: @@
 The operator "emp" denotes the empty heap constraint, the operator "pto" denotes the points-to predicate,
 the operator "sep" denotes separation start and is variadic, and the operator "wand" denote magic wand.
 A satisfiability relation <math>I,h \models_{SL} \varphi</math> is defined for <math>SL(T)_{Loc,Data}</math> formulas,
@@ Line 39: / Line 41: @@
 <math>h'\#h</math> denotes that heaps h' and h are disjoint.
 Notice that the arguments of "emp" are used to denote the type of the heap and have no meaning otherwise.
 =Syntax=
@@ Line 106: / Line 102: @@
    (assert (pto x (node 0 y z)))
    (check-sat)

@@ Line 19: / Line 19: @@
 | <math>I \models</math> L, if L is a T-literal
 |-
-| <math>I,h \models_{SL}</math> (emp t u)
+| <math>I,h \models_{SL}</math> (emp <math>t \ u</math>)
 | Iff
 | <math>h = \emptyset</math>
 |-
-| <math>I,h \models_{SL}</math> (pto t u)
+| <math>I,h \models_{SL}</math> (pto <math>t \ u</math>)
 | Iff
 | <math>h = \{(t^I,u^I)\} \text{ and } t^I\not=nil^I</math>
@@ Line 29: / Line 29: @@
 | <math>I,h \models_{SL} </math> (sep <math>\phi_1 \ldots \phi_n</math>)
 | Iff
-| there exist heaps <math>h_1,\ldots,h_n</math> s.t. <math>h=h_1\uplus \ldots \uplus h_2</math> and <math>I,h_i \models_{SL} \phi_i, i = 1,\ldots,n</math>
+| there exist heaps <math>h_1,\ldots,h_n</math> s.t. <math>h=h_1\uplus \ldots \uplus h_n</math> and <math>I,h_i \models_{SL} \phi_i, i = 1,\ldots,n</math>
 |-
 | <math>I,h \models_{SL}</math> (wand <math>\phi_1 \ \phi_2</math>)
@@ Line 36: / Line 36: @@
 |}
 Notice that the arguments of "emp" are used to denote the type of the heap and have no meaning otherwise.