data specification
using zbranch-array-sorted
znode := mkznode(. .parent : ref;
. .zbranches : zbranch-array;
. .leaf : bool;
. .dirty : bool;
. .usedsize : nat)
;
variables znd : znode;
end data specification