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