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

   export afs-asm

   import cache-asm

   using cache-asm, afs-asm, 
         cache-contracts


   

   by mapping cache_recovery# → afs_recovery#, cache_check_commit# → afs_check_commit#, cache_format# → afs_format#, 
              cache_sync# → afs_sync#, cache_fsync# → afs_fsync#, cache_fsyncdir# → afs_fsyncdir#, 
              cache_lookup# → afs_lookup#, cache_create# → afs_create#, cache_unlink# → afs_unlink#, 
              cache_mkdir# → afs_mkdir#, cache_rmdir# → afs_rmdir#, cache_link# → afs_link#, 
              cache_rename# → afs_rename#, cache_readpage# → afs_readpage#, cache_writepage# → afs_writepage#, 
              cache_readdir# → afs_readdir#, cache_evict# → afs_evict#, cache_truncate# → afs_truncate#, 
              cache_iget# → afs_iget#, cache_write_inode# → afs_write_inode#

   abstraction λ afs_dirs, afs_files, afs_asynced, cache_sync, cache_dirs, cache_files, cache_asynced, cache_icache, cache_dcache, cache_pcache. 
                 afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)
   ;

   
end asm refinement