deferred class interface ES_IO_DEVICE
   -- 
   --  Common abstraction of devices that provide unreliable service.
   -- 

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

invariant

    closed_is_not_open: closed = not open;

end of deferred ES_IO_DEVICE