Specification vfs-abs

[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
   posix-permission
, 
   afs-stream
, 
   vfs-permission
, 
   file-id-data, 
   posix-links

with
   

   
   
   functions  abs : directory-tree × nat → dir-heap → bool;
              abs : entries-tree × dir-entries → dir-heap → bool;
              abs| : directory-tree × nat × path × nat → dir-heap → bool;
              abs| : entries-tree × dir-entries × path × nat → dir-heap → bool;
              abs-files : file-heap → file-data-store;
              abs-of : open-files → open-file-handles;
              clinks : pathset × nat × dir-heap × file-heap → alink-set;
   
   
   variables  err2 : error;
              err3 : error;
              err4 : error;
              Pstr : string → dir-heap → bool;
              sdi : dir-entries;
              fpathtolink : path → alink;
   
   

   

   axioms clinks :  ⊦ alink ∈ clinks(ps, ino0, dirs, files) ↔ (∃ ino1, p. p ∈ ps ∧ ispath(p, ino0, ino1, dirs, files));
          abs-of-in :  ⊦ fd ∈ abs-of(of) ↔ fd ∈ of;
          used for: s, ls;
          abs-of-at : fd ∈ of ⊦ abs-of(of)[fd] = mkfh(⌜of[fd].ino⌝ , of[fd].mode, of[fd].pos);
          used for: s, ls;
          abs-fnode :  ⊦ abs(fnode(fid), ino) = (emp ∧ ⌜ino = fid.ino⌝ );
          used for: s, ls;
          abs-dnode :  ⊦ abs(dnode(md, sdt), ino) = _∃(λ ad. ino => ad * abs(sdt, ad.entries) ∧ ⌜ad.meta = md⌝  ∧ ⌜ad.size = # ad.entries⌝ );
          used for: ls;
          abs-empty :  ⊦ abs(∅, entries) = (⌜entries = ∅⌝  ∧ emp);
          used for: s, ls;
          abs-rec :  ⊦ ¬ name ∈ sdt → abs(sdt[name, tree], entries) = (⌜name ∈ entries⌝  ∧ abs(tree, entries[name]) * abs(sdt, entries -- name));
          used for: ls;
          abs-files-in :  ⊦ ⌜ino⌝  ∈ abs-files(files) ↔ ino ∈ files;
          used for: s, ls;
          abs-files-at :  ⊦ ino ∈ files → abs-files(files)[⌜ino⌝ ] = mkfile(files[ino].meta, (files[ino].content.stream to files[ino].size).buf);
          used for: s, ls;
          absc-emp :  ⊦ abs|(tree, ino, ε, ino0) = (emp ∧ ⌜ino = ino0⌝ );
          used for: s, ls;
          absc-dnode
          : ⊦   p ≠ ε
              →   abs|(dnode(md, sdt), ino, p, ino0)
                = _∃(λ ad. ino => ad * abs|(sdt, ad.entries, p, ino0) ∧ ⌜ad.meta = md⌝  ∧ ⌜ad.size = # ad.entries⌝ );
          used for: ls;
          absc-entries
          :  ⊦ abs|(sdt, entries, str ' + p, ino0) = (⌜str ∈ entries⌝  ∧ abs|(sdt[str], entries[str], p, ino0) * abs(sdt -- str, entries -- str));
          used for: ls;

   

   
end enrich