DEFINITION MODULE ADDRESS;

(* I/O Module for Type ADDRESS *)

FROM SYSTEM IMPORT ADDRESS;
FROM FileIO IMPORT File;

(* EBNF of the textual representation of ADDRESS values:

    addressValue :
       digitGroup digitGroup ( groupSeparator? digitGroup digitGroup )* ;
    digitGroup : base16Digit base16Digit ;
    base16Digit : "0" .. "9" | "A" .. "F" ;
    groupSeparator : " " | "." | ":" ;

    static semantics:

    ADDRESS values are always left padded with zeroes to the length
    required to represent the maximum value of type ADDRESS. *)

PROCEDURE Read ( infile : File; VAR adr : ADDRESS );
(* Reads the textual representation of an ADDRESS value from stream infile
   - any leading whitespace is skipped
   - any remaining characters that are part of the value being read are
     removed from infile
   - the textual representation of the value read is assigned to adr
   - the file status is set to any of:
     success, outOfRange, wrongFormat, endOfLine, or endOfInput. This
   procedure is substituted for invocations of READ with an ADDRESS argument.*)

PROCEDURE Write ( outfile : File; adr : ADDRESS );
(* Writes the value of ADDRESS adr in standard format to stream outfile. This
   procedure is substituted for invocations of WRITE with an ADDRESS argument.*)

PROCEDURE WriteF ( outfile      : File;
                   CONST fmtStr : ARRAY OF CHAR;
                   items        : VARIADIC OF ADDRESS );
(* Writes a formatted textual representation of one or more ADDRESS values to
   output stream outfile. The output format is determined by fmtStr. This
   procedure is substituted for invocations of WRITEF with one or more
   ADDRESS arguments. *)

END ADDRESS.