generic data specification parameter binheap-key using nat keyindex := key-index(. .key : key;. .idx : nat) ; variables ki : keyindex; end generic data specification