class interface ES_STREAM_SOCKET
   -- 
   --  A socket that sends and receives streamed data.
   -- 

creation
   make
      --  Create an INET4 (e.g. normal internet) socket.
      ensure
         open_or_error: not error = open;
         not_yet_connected: not connected;
         not_yet_sent: characters_sent = 0

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 socket open?

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

   id: INTEGER
      --  Unique identifier for this socket

feature(s) from ES_IO_DEVICE
   --  Lifecycle

   close
      --  Close the socket 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

feature(s) from ES_IMPORTED_EXTERNALS
   --  Once

   externals_: ES_EXTERNALS
      --  Access those compatability commands.

feature(s) from ES_STREAM_SOCKET
   --  Accessors

   connected: BOOLEAN
      --  Are we connected to a remote host?

   end_of_data: BOOLEAN
      --  Has the remote host closed its write stream?

   remote_address: STRING
      --  The remote address
      require
         connected: connected
      ensure
         still_connected: connected;
         not_void: Result /= Void;
         clone: equal(Result,remote_address_rep) and Result /= remote_address_rep

   remote_port: INTEGER
      --  The remote port
      require
         connected: connected
      ensure
         still_connected: connected

feature(s) from ES_STREAM_SOCKET
   --  Read and Write

   send (data: STRING; offset: INTEGER)
      --  Send as much of data as possible starting from offset.
      require
         connected: connected;
         data_present: data /= Void and then not data.empty;
         good_offset: offset >= 0 and offset < data.count
      ensure
         still_connected: connected;
         error_state: error = characters_sent = 0;
         count_sent: not error implies characters_sent > 0 and characters_sent <= data.count - offset

   characters_sent: INTEGER
      --  The number of characters sent by the last send.

   send_all (data: STRING)
      --  Send all of data.
      require
         connected: connected;
         data_present: data /= Void and then not data.empty
      ensure
         still_connected: connected;
         error_state: error or not error

   receive
      --  Read data.
      require
         connected: connected;
         more_data: not end_of_data
      ensure
         still_connected: connected;
         data_received: (not error and not end_of_data) = received_data /= Void and then not received_data.empty

   received_data: STRING
      --  Data returned from the last receive

feature(s) from ES_STREAM_SOCKET
   --  Lifecycle

   connect (address: STRING; port: INTEGER)
      --  Connect to the remote address.
      require
         open: open;
         not_yet_connected: not connected;
         not_void: address /= Void;
         valid_port: port >= 1 and port <= 65535
      ensure
         still_open: open;
         connected_or_error: not error = connected;
         to_correct_host: connected implies equal(remote_address,address) and remote_port = port

   send_end_of_data
      --  Close the output half of the socket. An end_of_data
      --  will be sent.
      require
         connected: connected
      ensure
         technically_still_connected: connected;
         may_have_error: error or not error

invariant

    closed_is_not_open: closed = not open;

    only_connected_when_open: connected implies open;

end of ES_STREAM_SOCKET