data specification using nat, volid data types lebref := none | . × .(. .vol : volid;. .leb : nat) ; variables lref : lebref; end data specification