deferred class interface F_ASYNCH_IO

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, 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


end of deferred F_ASYNCH_IO