deferred class interface F_FINITE_STREAM

feature(s) from F_STREAM
   --  Constant

   Byte_maximum: INTEGER

feature(s) from F_STREAM
   --  Access

   connect
      --  Connect the stream so that it may, if the connect is successful, 
      --  be accessible.

      ensure
         can_fail:  --  success implies is_alive

   imperative_connect
      --  Connect the stream and generate an exception if connection fails.

      ensure
         valid: is_alive

   disconnect
      --  Disconnect a valid stream.

      require
         valid: is_alive
      ensure
         done: not is_alive

feature(s) from F_STREAM
   --  Status

   is_alive: BOOLEAN
      --  Is the stream connection alive (allowing read/write)?


   has_data: BOOLEAN
      --  Is at least one byte waiting to be read?

      require
         valid: is_alive

   has_error: BOOLEAN
      --  Is the stream in an error state?


   is_readable: BOOLEAN
      --  Is the stream readable?


   is_writable: BOOLEAN
      --  Is the stream writable?


feature(s) from F_STREAM
   --  Read/write

   last_byte: INTEGER
      --  Last byte read.

      ensure
         byte_size: Result >= 0 and then Result <= Byte_maximum

   read_byte
      --  Read one byte and update last byte.

      require
         valid: is_alive;
         readable: is_readable;
         available: has_data

   write_byte (byte: INTEGER)
      --  Write a byte.

      require
         valid: is_alive;
         writable: is_writable;
         byte_size: byte >= 0 and then byte <= Byte_maximum

feature(s) from F_FINITE_STREAM
   --  Position

   set_position (idx: INTEGER)
      --  Set current position in stream.

      require
         alive: is_alive;
         valid_pos: idx >= 1 and idx <= size
      ensure
         done: not has_error implies position = idx

   position: INTEGER
      --  Current position in the stream.

      require
         alive: is_alive
      ensure
         bounds: position >= 1 and position <= size

   size: INTEGER
      --  Current size of stream in bytes.

      require
         alive: is_alive


end of deferred F_FINITE_STREAM