data specification using nat ref-node := rnode(. .leb : nat) ; variables rnd : ref-node; rnd0 : ref-node; rnd1 : ref-node; end data specification