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

   export index-asm


   import btree-asm

   using btree-asm, 
         index-asm


   

   by mapping btree_recover# → index_recover#, btree_index_contains# → index_index_contains#, 
              btree_index_lookup# → index_index_lookup#, btree_index_store# → index_index_store#, 
              btree_index_remove# → index_index_remove#, btree_index_truncate# → index_index_truncate#, 
              btree_index_entries# → index_index_entries#, btree_get_leb_size → index_get_leb_size, btree_read_gnd# → index_read_gnd#, 
              btree_read_gblock_nodes# → index_read_gblock_nodes#, btree_get_gc_block# → index_get_gc_block#, 
              btree_add_gnds# → index_add_gnds#, btree_sync# → index_sync#, 
              btree_set_gblock_refsize# → index_set_gblock_refsize#, btree_get_gblock_refsize# → index_get_gblock_refsize#, 
              btree_get_block_free_size# → index_get_block_free_size#, btree_is_log_empty# → index_is_log_empty#, 
              btree_allocate_gnd# → index_allocate_gnd#, btree_deallocate_gnd# → index_deallocate_gnd#, 
              btree_commit# → index_commit#, btree_requires_commit# → index_requires_commit#, btree_format# → index_format#

   abstraction   PINVAL = GINVAL ∧ PSTORE = GSTORE ∧ PSTORE0 = GSTORE0 ∧ PNL = NL ∧ PMAXINO = MAXINO ∧ P_OS = OS
               ∧ btree-inv(RT, ROOTADR, ISTORE, ISTORE0, ZH, PRI, PFI) ∧ RI = PRI ∧ FI = PFI ∧ (ISYNCED ↔ PSYNCED)
   ;

   
end asm refinement