Specification separation-rg

[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 maplet , 
       gownership with
   functions 
      ! : id × (ref → id) × (heap → bool) → heap → bool;
       . * . : (heap × heap → bool) × (heap × heap → bool) → heap × heap → bool prio 10;
      ↑ . : (heap → bool) → heap × heap → bool;
      ↓ . : (heap → bool) → heap × heap → bool;
   predicates 
      rely : id × (ref → id) × heap × (ref → id) × heap;
      guar : id × (ref → id) × heap × (ref → id) × heap;
   variables 
      me : id; 
      O0, O1, O2 : ref → id; 
      R, R0, R1, R2 : heap × heap → bool; 
      Q : heap → bool; 
      H3, H4, H5 : heap; 
   
   axioms 
      old :  ⊦ (↓ P)(H0, H1) ↔ P(H0);
      new :  ⊦ (↑ P)(H0, H1) ↔ P(H1);
      used for : s, ls;
       
      sep :  ⊦ (R0 * R1)(H0, H1) ↔ (∃ H2, H3, H4, H5. H2 ⊥ H3 ∧ H4 ⊥ H5 ∧ H2 ∪ H3 = H0 ∧ H4 ∪ H5 = H1 ∧ R0(H2, H4) ∧ R1(H3, H5));
      rely :  ⊦ rely(me, O1, H1, O2, H2) ↔ (∀ r. (O1(r) = me ↔ O2(r) = me) ∧ (O1(r) = me → (r ∈ H1 ↔ r ∈ H2) ∧ (r ∈ H1 → H1[r] = H2[r])));
      guar :  ⊦ guar(me, O1, H1, O2, H2) ↔ (∀ id. id ≠ me → rely(id, O1, H1, O2, H2));
      owned :  ⊦ !(id, O, P)(H) ↔ P(H) ∧ (∀ r. r ∈ H → O(r) = id);
end enrich