[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 implementation-refines-caterpillar
asm refinement
   

   export caterpillar-asm


   import implementation-asm


   using implementation-asm
, 
         caterpillar-asm


   

   by mapping tree_buffer_heap_init# → caterpillar_init#, tree_buffer_heap_add# → caterpillar_add#, 
              tree_buffer_heap_get# → caterpillar_get#

   abstraction λ h0, xs, xs_len0, ys, H, rxs, rys, h, xs_len, to_delete. 
                 ∃ n. 
                   ((ls(rxs, xs) * ls(rys, ys) * del-list(to_delete, n)))(H) ∧ n ≤ # xs + # ys ∧ n + # xs ≤ h ∧ h = h0 ∧ xs_len = xs_len0
   ;

   
end asm refinement