deferred class interface F_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 end of deferred F_STREAM