deferred class interface F_SOCKET feature(s) from F_STREAM -- Constant Byte_maximum: INTEGER feature(s) from F_STREAM -- Access connect -- Open TCP connection. ensure can_fail: -- success implies is_alive imperative_connect -- Connect, exception violation if it fails. ensure valid: is_alive disconnect -- End asynchronous file operation. -- Note: when_died is called. require valid: is_alive ensure done: not is_alive feature(s) from F_STREAM -- Status is_alive: BOOLEAN -- Current connection alive? has_data: BOOLEAN -- Data waiting (connection alive for asynchronous file). require valid: is_alive has_error: BOOLEAN -- Error status (not is_alive)/ 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 -- Result of last read operation. ensure byte_size: Result >= 0 and then Result <= Byte_maximum read_byte -- Read a byte, call when_read when byte read. require valid: is_alive; readable: is_readable; available: has_data ensure writing: -- is_writing write_byte (byte: INTEGER) -- Asynchronous write byte. -- when_written called when operation terminates. require valid: is_alive; writable: is_writable; byte_size: byte >= 0 and then byte <= Byte_maximum feature(s) from MEMORY -- Removal : dispose -- Close file handle. ensure done: handle = Invalid_handle_value full_collect -- Force a full collection cycle if garbage collection is -- enabled; do nothing otherwise. feature(s) from F_ASYNCH_STREAM -- Status of asynchronous communications is_connect_readable: BOOLEAN -- Open mode: read. is_connect_writable: BOOLEAN -- Open mode: write. is_reading: BOOLEAN -- Asynchronous read under way. is_writing: BOOLEAN -- Asynchronous write under way. feature(s) from F_ASYNCH_IO -- Default writing interface --? remove from base class push_byte (byte: INTEGER) -- Push byte onto file (queue if file busy). require alive: is_alive; ok: byte >= 0 and byte <= Byte_maximum push_string (str: STRING) -- Push string onto file (queue if busy). -- (the string is transmitted as is, without anything, like newline, added). require ok: str /= Void; alive: is_alive; -- for_all n, str.item (n).code <= Byte_maximum narrow: when_written -- Previous byte written. require finished: not is_writing feature(s) from F_SOCKET -- Setup set_address (ip_address: IP_ADDRESS) require closed: not is_alive set_port (port_id: INTEGER) -- Set TCP port require ok: port_id >= 0; closed: not is_alive end of deferred F_SOCKET