[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 vfs-base
enrich
   afs-asm
, 
   open-files, 
   nat-set
, 
   align

with
   

   
   
   functions  min : nat × nat × nat → nat;
   predicates  of-cons : open-files × dir-heap × file-heap;
               zero-cons : file-heap;
               zero-cons : nat × file-heap;
               is-open : nat × open-files;
               valid-content : file-heap;
   
   
   
   

   

   axioms valid-content :  ⊦ valid-content(files) ↔ (∀ ino. ino ∈ files → valid-content(ino, files));
          of-cons :  ⊦ of-cons(of, dirs, files) ↔ (∀ n. n ∈ of → of[n].ino ∈ files);
          zero-cons :  ⊦ zero-cons(files) ↔ (∀ ino. ino ∈ files → zero-cons(ino, files));
          min3 :  ⊦ min(n0, n1, n2) = min(n0, min(n1, n2));
          is-open :  ⊦ is-open(ino, of) ↔ (∃ n. n ∈ of ∧ of[n].ino = ino);

   

   
end enrich