deferred class interface F_ASYNCH_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 currently readable? ensure asynch: Result implies not is_reading is_writable: BOOLEAN -- Is the stream currently writable? ensure asynch: Result implies not is_writing 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_ASYNCH_STREAM -- Status of asynchronous communications is_connect_readable: BOOLEAN -- Is the stream open in read mode? is_connect_writable: BOOLEAN -- Is the stream open in write mode? is_reading: BOOLEAN -- Is a read operation currently under way? is_writing: BOOLEAN -- Is a write operation currently under way? end of deferred F_ASYNCH_STREAM