[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 posix-base
enrich
   file-data-store
, 
   directory-tree-fids
, 
   open-file-handles-ext

with
   

   
   
   functions  . .fids : open-file-handles → fidset;
              meta : path × directory-tree × file-data-store → metadata;
   predicates  fids-cons : directory-tree × file-data-store × open-file-handles;
               posix-crash : directory-tree × file-data-store × open-file-handles × directory-tree × file-data-store × open-file-handles;
   
   variables  path : path;
              path' : path;
              root : directory-tree;
   
   

   

   axioms ofh-fids :  ⊦ fid ∈ ofh.fids ↔ (∃ n. n ∈ ofh ∧ ofh[n].fid = fid);
          used for: ls;
          fids-cons :  ⊦ fids-cons(root, fs, ofh) ↔ (∀ fid. fid ∈ fs ↔ fid ∈ root.fids ∨ fid ∈ ofh.fids);
          inf-fids :  ⊦ ∃ fid. ¬ fid ∈ dom fs;
          inf-ofh :  ⊦ ∃ fd. ¬ fd ∈ dom ofh;
          meta-file : ¬ tree[p].dir? ⊦ meta(p, tree, fs) = fs[tree[p].fid].meta;
          used for: s, ls;
          meta-dir : tree[p].dir? ⊦ meta(p, tree, fs) = tree[p].meta;
          used for: s, ls;
          posix-crash
          : ⊦   posix-crash(tree0, fs0, ofh0, tree1, fs1, ofh1)
              ↔ ofh1 = ∅ ∧ tree1 = tree0 ∧ (∀ fid. fid ∈ fs1 ↔ fid ∈ tree1.fids ∧ fid ∈ fs0) ∧ (∀ fid. fid ∈ fs1 → fs1[fid] = fs0[fid]);

   

   
end enrich