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
   relops, 
   heap, 
   heap-sep
with
   functions 
       modify : Set[Ref[A]] → Heap[A] × Heap[A] → Bool;
       modify* : Set[Ref[A]] → Heap[A] × Heap[A] → Bool;
       . ≡ . : Heap[A] × Heap[A] → Set[Ref[A]] → Bool;
   
   predicates 
       footprint : Set[Ref[A]] × (Heap[A] → Bool) × Heap[A];
   
   variables 
       h : Heap[A];
       r : Ref[A];
       rs : Set[Ref[A]];
       hP : Heap[A] → Bool;
       ob : A;
   
   
   axioms 
      modify: 
        modify(rs)(h0, h1)
      ↔   (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h1 = h0 ++ r) ∨ (∃ r, obj. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0(r := obj))
        ∨ (∃ 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