[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,

Specification rg
enrich embed-aux with
   predicates 
      rely : aux × refset × (ref → obj) × (ref → aux) × refset × (ref → obj) × (ref → aux);
      owns-none : aux × refset × (ref → aux);
      owns-one : aux × ref × refset × (ref → aux);
   variables 
      f, f0, f1 : ref → obj; 
      g, g0, g1 : ref → aux; 
   
   axioms 
      rely :  ⊦ rely(a, rs0, f0, g0, rs1, f1, g1) ↔ (∀ r. (g0(r) = a ∧ r ∈ rs0 ↔ g1(r) = a ∧ r ∈ rs1) ∧ (g0(r) = a ∧ r ∈ rs0 → f0(r) = f1(r)));
      used for : ls;
       
      owns-none :  ⊦ owns-none(a, rs, g) ↔ (∀ r. r ∈ rs → g(r) ≠ a);
      used for : ls;
       
      owns-one :  ⊦ owns-one(a, r, rs, g) ↔ r ≠ null ∧ r ∈ rs ∧ g(r) = a ∧ (∀ r0. r0 ∈ rs ∧ r0 ≠ r → g(r0) ≠ a);
      used for : ls;
       
end enrich