[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 zheap
actualize
   separation-all

with
   znode, 
   address-set-array


   
by morphism
   :heap → zheap; 
   :obj → znode; 
   :elem → address-set-array; 
   ∅ → ∅; 
   ++ → ++; 
   -- → --; 
   [ ] → [ ]; 
   [ ] → [ ]; 
   # → #; 
   ∪ → ∪; 
   \ → \; 
   \ → \; 
   * → *; 
   ⊗ → ⊗; 
   -* → -*; 
   -⊗ → -⊗; 
   ¬ → not; 
   ∧ → and; 
   ∨ → or; 
   → → ->; 
   ⌜ ⌝ → ⌜ ⌝; 
   { } → { }; 
   ite → ite; 
   => → =>; 
   =>_ → =>_; 
   =>? → =>?; 
   _∃ → _∃; 
   _∃ → _∃; 
   _∃ → _∃; 
   ⊗_ → ⊗_; 
   _∃ → _∃; 
   ∈ → ∈; 
   ⊆ → ⊆; 
   ⊥ → ⊥; 
   emp → emp; 
   true → true; 
   false → false; 
   precise → precise; 
   ⊆ → ⊆; 
   ≡ → ≡; 
   a → asar; 
   b → asar0; 
   c → asar1; 
   H → zh; 
   H0 → zh0; 
   H1 → zh1; 
   H2 → zh2; 
   o → znd; 
   o0 → znd0; 
   o1 → znd1; 
   rP → rP; 
   rrP → rrP; 
   oP → oP; 
   P → P; 
   P0 → P0; 
   P1 → P1; 
   P2 → P2; 
   nP → nP; 
   Pa → Pa
end actualize