Specification heap-mod

[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
   rtc-heap, 
   heap-sep
with
   functions  modify : refset → heap × heap → bool;
              modify* : refset → heap × heap → bool;
              . ≡ . : heap × heap → refset → bool;
   predicates  footprint : refset × (heap → bool) × heap;
   variables  h : heap;
              r : ref;
              rs : refset;
              hP : heap → bool;
   axioms 
      modify
      : ⊦   modify(rs)(h0, h1)
          ↔   (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h1 = h0 ++ r) ∨ (∃ r, o. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0[r, o])
            ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0 -- r);
      modify+ :  ⊦ modify*(rs)(h0, h1) ↔ modify(rs) ^*(h0, h1);
      footprint :  ⊦ footprint(rs, hP, h0) ↔ (∀ h1. modify*(rs)(h0, h1) → (hP(h0) ↔ hP(h1)));
      agree :  ⊦ ((h0 ≡ h1))(rs) ↔ (∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]));

   
end enrich