data specification using key-index-array , nat-pot binheap := bin-heap(. .ar : key-array;. .size : nat) ; variables bh : binheap; bh0 : binheap; end data specification