Specification vfs-permission

[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,

instantiate parameter
   permission-param

< 
   path-permission

with 
   vfs-base, 
   permission


   
by mapping
      : state → nat × dir-heap × file-heap; 
      meta → meta; 
      st → ino, dirs, files
   rename 
      px → px; 
      px-parent → px-parent; 
      py → py; 
      pr → pr; 
      pw → pw
end instantiate