data asm specification 
   tree_buffer_heap

   using linked-list-seg
, 
         del-lists

   

   
   
   
   
   procedures tree_buffer_heap_init# nat :  : heap × ref × ref × nat × nat × reflist  ;
              tree_buffer_heap_process_one#  : heap × reflist nonfunctional ;
              tree_buffer_heap_process_queue#  : heap × reflist nonfunctional ;
              tree_buffer_heap_add# elem × nat : heap × ref × ref × nat × reflist nonfunctional nondeterministic;
              tree_buffer_heap_get# heap × ref × ref × nat :  : list  ;
   variables  h : nat;
              rxs : ref;
              rys : ref;
              xs_len : nat;
              to_delete : reflist;
   
   

   axioms infinite-memory :  ⊦ ∃ r. r ≠ null ∧ ¬ r ∈ H;

   state variables  H : heap;
                    rxs : ref;
                    rys : ref;
                    h : nat;
                    xs_len : nat;
                    to_delete : reflist;

   initialization procedure tree_buffer_heap_init#

   

   sequential

      
   
      

   

   

   

   

   

   

   

   

   

   

   declarations init:
                tree_buffer_heap_init#(n0; ; H, rxs, rys, h, xs_len, to_delete)
                  precondition n0 > 0;
                {{h := n0; rxs := null; rys := null; to_delete := []; xs_len := 0; H := ∅}
                }
                process-one
                : tree_buffer_heap_process_one#(; H, to_delete)
                  {if to_delete ≠ []
                   then let r = to_delete.head
                        in {to_delete := to_delete.tail; if H[r].nxt ≠ null then to_delete := H[r].nxt + to_delete; H := H -- r}
                  }
                ;
                process-queue
                : tree_buffer_heap_process_queue#(; H, to_delete)
                  {tree_buffer_heap_process_one#(; H, to_delete); tree_buffer_heap_process_one#(; H, to_delete)}
                ;
                add:
                tree_buffer_heap_add#(a, h; H, rxs, rys, xs_len, to_delete)
                {{tree_buffer_heap_process_queue#(; H, to_delete); 
                  choose r
                  with ¬ r ∈ H ∧ r ≠ null
                  in {H := H ++ r; H[r].val := a; H[r].nxt := rxs; 
                      if xs_len + 1 = h
                      then {if rys ≠ null then to_delete := rys + to_delete; rys := r; xs_len := 0; rxs := null}
                      else {rxs := r; xs_len := 1 + xs_len}}}
                }
                get:
                tree_buffer_heap_get#(H, rxs, rys, h; ; x)
                {{x := []; 
                  let n = 0, r = rxs
                  in {while n < h ∧ r ≠ null do {x := x + H[r].val; r := H[r].nxt; n := n + 1}; r := rys; 
                      while n < h ∧ r ≠ null do {x := x + H[r].val; r := H[r].nxt; n := n + 1}}}
                }
end data asm specification