[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 : ref → obj;
              g : ref → aux;
              r : ref;
              rs : refset;
              a : aux;
              o : obj;
              hP : heap → bool;
   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: lws;

   
end enrich