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

   export afs-asm


   import aubifs-asm

   using aubifs-asm, 
         afs-asm
, 
         aubifs-abs

   

   by mapping aubifs_replay# → afs_recovery#, aubifs_gc# → { ASYNCED := ? }, aubifs_check_commit# → afs_check_commit#, 
              aubifs_format# → afs_format#, aubifs_sync# → afs_sync#, aubifs_fsync# → afs_fsync#, 
              aubifs_fsyncdir# → afs_fsyncdir#, aubifs_lookup# → afs_lookup#, aubifs_create# → afs_create#, 
              aubifs_unlink# → afs_unlink#, aubifs_mkdir# → afs_mkdir#, aubifs_rmdir# → afs_rmdir#, 
              aubifs_link# → afs_link#, aubifs_rename# → afs_rename#, aubifs_readpage# → afs_readpage#, 
              aubifs_writepage# → afs_writepage#, aubifs_readdir# → afs_readdir#, aubifs_evict# → afs_evict#, 
              aubifs_truncate# → afs_truncate#, aubifs_iget# → afs_iget#, aubifs_write_inode# → afs_write_inode#

   abstraction DIRS = abs-dirs(FS, RI) ∧ FILES = abs-files(FS, RI) ∧ orphans(DIRS, FILES) = abs-keys(RO) ∧ (ASYNCED → CSYNCED);

   internal equivalence DIRS` = DIRS ∧ FILES` = FILES;
end asm refinement