data specification using nat, volid lebadress := . × .(. .vol : volid;. .leb : nat) ; variables ladr : lebadress; end data specification