kdrag.theories.logic.sep
Functions
|
Classes
|
A model of seperation logic using sets as a partial monoid. |
- class kdrag.theories.logic.sep.Sep(KeySort: SortRef)
Bases:
objectA model of seperation logic using sets as a partial monoid.
>>> Sep8 = make_sep(smt.BitVecSort(8)) >>> p, q = Sep8.Props("p q") >>> h = smt.Const("h", Sep8.AllocSort) >>> _ = kd.prove(smt.ForAll([h], Sep8.Sep(p, q)[h] == Sep8.Sep(q, p)[h])) >>> _ = kd.prove(smt.ForAll([h], Sep8.Sep(p, Sep8.Emp)[h] == p[h]))
- Parameters:
KeySort (SortRef)
- Alloc(key)
Alloc(key) is a predicate that exactly key is allocated in current heap
>>> Sep8 = make_sep(smt.BitVecSort(8)) >>> key = smt.BitVec("key", 8) >>> Sep8.Alloc(key) Lambda(h!..., h!... == Store(K(BitVec(8), False), key, True))
- And(*args)
Lifted And
>>> Sep8 = make_sep(smt.BitVecSort(8)) >>> p, q = Sep8.Props("p q") >>> Sep8.And(p, q) Lambda(h!..., And(p[h!...], q[h!...]))
- Implies(a: PropRef, b: PropRef) PropRef
- Parameters:
a (PropRef)
b (PropRef)
- Return type:
PropRef
- Lift(expr: ExprRef)
Lift an expression into constant function on heap.
>>> Sep8 = make_sep(smt.BitVecSort(8)) >>> p = smt.Int("p") >>> Sep8.Lift(p) Lambda(h!..., p)
- Parameters:
expr (ExprRef)
- Or(*args)
- Prop(name: str)
A named separation logic proposition
- Parameters:
name (str)
- Props(names: str)
- Parameters:
names (str)
- Pto(key, v)
Pto(key, v) says that key is allocated but separately a special variable call heap has value v at location key.
>>> Sep8 = make_sep(smt.BitVecSort(8)) >>> key = smt.BitVec("key", 8) >>> v = smt.BitVec("v", 8) >>> Sep8.Pto(key, v) Lambda(h!..., And(Lambda(h!..., h!... == Store(K(BitVec(8), False), key, True))[h!...], Lambda(h!..., heap[key] == v)[h!...]))
- Sep(a, b)
Separating conjunction
- Valid(prop: PropRef) BoolRef
Valid converts a predicate on heaps into the boolean expression stating it is true for all heaps (semantically valid).
- Parameters:
prop (PropRef)
- Return type:
BoolRef
- Wand(a, b)