Specification heap-sep

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,
enrich
   heap
with
   functions  . * . : (heap → bool) × (heap → bool) → heap → bool prio 10 right;
              . ⊗ . : (heap → bool) × (heap → bool) → heap → bool prio 10 right;
              . -* . : (heap → bool) × (heap → bool) → heap → bool;
              . -⊗ . : (heap → bool) × (heap → bool) → heap → bool;
              not . : (heap → bool) → heap → bool;
              . and . : (heap → bool) × (heap → bool) → heap → bool prio 4 right;
              . or . : (heap → bool) × (heap → bool) → heap → bool prio 3 right;
              . -> . : (heap → bool) × (heap → bool) → heap → bool prio 2 right;
              ⌜ . ⌝ : bool → heap → bool;
              { . } : heap → heap → bool;
              ite : bool × (heap → bool) × (heap → bool) → heap → bool;
   predicates  emp : heap;
               true : heap;
               false : heap;
               precise : (heap → bool);
               . ⊆ . : (heap → bool) × (heap → bool);
   variables  hP : heap → bool;
              bv : bool;
              h : heap;
   axioms 
      ite :  ⊦ ite(bv, hP0, hP1) = (bv ⊃ hP0;hP1);
      used for: ls;
      emp :  ⊦ emp(h) ↔ h = ∅;
      used for: s, ls;
      true :  ⊦ true = ⌜true⌝ ;
      used for: ls;
      false :  ⊦ false = ⌜false⌝ ;
      used for: ls;
      sep :  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1));
      sharing :  ⊦ ((hP0 ⊗ hP1))(h) ↔ (∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ hP0(h0 ∪ h2) ∧ hP1(h1 ∪ h2));
      wand :  ⊦ ((hP0 -* hP1))(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h));
      septract :  ⊦ ((hP0 -⊗ hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h ∧ h1 = h0 ∪ h ∧ hP0(h0) ∧ hP1(h1));
      not :  ⊦ (¬ hP0)(h) ↔ ¬ hP0(h);
      used for: s, ls;
      and :  ⊦ ((hP0 ∧ hP1))(h) ↔ hP0(h) ∧ hP1(h);
      used for: s, ls;
      or :  ⊦ ((hP0 ∨ hP1))(h) ↔ hP0(h) ∨ hP1(h);
      used for: s, ls;
      imp :  ⊦ ((hP0 → hP1))(h) ↔ hP0(h) → hP1(h);
      used for: s, ls;
      prop :  ⊦ ⌜bv⌝ (h) ↔ bv;
      used for: s, ls;
      this :  ⊦ {h} (h0) ↔ h = h0;
      used for: s, ls;
      precise :  ⊦ precise(hP) ↔ (∀ h, h0, h1, h2. hP(h) ∧ hP(h0) ∧ h ⊥ h1 ∧ h0 ⊥ h2 ∧ h ∪ h1 = h0 ∪ h2 → h = h0);
      Imp :  ⊦ hP0 ⊆ hP1 ↔ (∀ h. hP0(h) → hP1(h));

   
end enrich