[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 file-heap
actualize
   separation

with
   abstract-file


   
by morphism
   :heap → file-heap; 
   :ref → nat; 
   :obj → abstract-file; 
   :refset → nat-set; 
   null → 0; 
   ∅ → ∅; 
   ∅ → ∅; 
   =>_ → =>af; 
   =>? → =>af?; 
   ++ → ++; 
   # → #; 
   { } → { }; 
   ∪ → ∪; 
   ∩ → ∩; 
   \ → \; 
   -- → --; 
   ++ → ++; 
   -- → --; 
   [ ] → [ ]; 
   [ ] → [ ]; 
   # → #; 
   ∪ → ∪; 
   \ → \; 
   \ → \; 
   * → *; 
   ⊗ → ⊗; 
   -* → -*; 
   -⊗ → -⊗; 
   ¬ → not; 
   ∧ → and; 
   ∨ → or; 
   → → ->; 
   ⌜ ⌝ → ⌜ ⌝; 
   { } → { }; 
   ite → ite; 
   => → =>; 
   _∃ → _∃; 
   _∃ → _∃; 
   _∃ → _∃; 
   ∈ → ∈; 
   ⊆ → ⊆; 
   ∈ → ∈; 
   ⊆ → ⊆; 
   ⊥ → ⊥; 
   emp → emp; 
   true → true; 
   false → false; 
   precise → precise; 
   ⊆ → ⊆; 
   ≡ → ≡; 
   H → files; 
   H0 → files0; 
   H1 → files1; 
   H2 → files2; 
   r → ino; 
   r0 → ino0; 
   r1 → ino1; 
   o → af; 
   o0 → af0; 
   o1 → af1; 
   rs → ns; 
   rs0 → ns0; 
   rs1 → ns1; 
   rs2 → ns2; 
   rP → nF; 
   rrP → nnF; 
   oP → adF; 
   P → F; 
   P0 → F0; 
   P1 → F1; 
   P2 → F2
end actualize