deferred class interface ES_NON_BLOCKING_DEVICE
   -- 
   --  A device that can be selectively set not to block on I/O.
   -- 

feature(s) from ES_IMPORTED_EXTERNALS
   --  Once

   externals_: ES_EXTERNALS
      --  Access those compatability commands.

feature(s) from ES_IO_DEVICE
   --  Accessors

   error: BOOLEAN
      --  Did the last operation result in an error?

   error_name: STRING
      --  Description of the error
      require
         error_present: error
      ensure
         not_void: Result /= Void

   error_code: INTEGER
      --  Unique code for the error
      require
         error_present: error

   open: BOOLEAN
      --  Is this device active?

   closed: BOOLEAN
      --  Has this device been rendered inactive, its resources freed?

   id: INTEGER
      --  Unique identifier.

feature(s) from ES_IO_DEVICE
   --  Lifecycle

   close
      --  Close the connection and free resources.
      require
         open: open
      ensure
         closed: closed

feature(s) from ES_NON_BLOCKING_DEVICE
   --  Non blocking control

   non_blocking: BOOLEAN
      --  Has this device been set non-blocking?

   set_non_blocking
      --  Make this device non-blocking
      ensure
         set: not error = non_blocking

   was_last_error_blocking: BOOLEAN
      --  Was the last error an "otherwise would block" situation?
      require
         has_error: error

invariant

    closed_is_not_open: closed = not open;

end of deferred ES_NON_BLOCKING_DEVICE