[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-refine
asm refinement
   

   export posix-asm


   import vfs-asm

   using vfs-asm, 
         posix-asm
, 
         vfs-abs, vfs-contracts


   

   by mapping vfs_recover# → posix_recover#, vfs_format# → posix_format#, vfs_mkdir# → posix_mkdir#, 
              vfs_rmdir# → posix_rmdir#, vfs_create# → posix_create#, vfs_open# → posix_open#, 
              vfs_close# → posix_close#, vfs_read# → posix_read#, vfs_write# → posix_write#, vfs_seek# → posix_seek#, 
              vfs_rename# → posix_rename#, vfs_link# → posix_link#, vfs_unlink# → posix_unlink#, 
              vfs_truncate# → posix_truncate#, vfs_readmeta# → posix_readmeta#, vfs_writemeta# → posix_writemeta#, 
              vfs_readdir# → posix_readdir#, vfs_sync# → posix_sync#, vfs_fsync# → posix_fsync#, 
              vfs_fsyncdir# → posix_fsyncdir#

   abstraction OFH = abs-of(OF) ∧ FS = abs-files(FILES) ∧ abs(ROOT, ROOT_INO)(DIRS) ∧ (PSYNCED → ASYNCED);

   
end asm refinement