data specification using nat, file-id, file-mode file-handle := mkfh(. .fid : fid;. .mode : file-mode;. .pos : nat) ; variables fh : file-handle; end data specification