class interface ES_SERVER_SOCKET
   -- 
   --  A socket that waits for remote hosts to connect, and creates
   --  STREAM_SOCKET's to handle those connections.
   -- 

creation
   make
      --  Create an ES_SERVER_SOCKET
      ensure
         open_or_error: not error = open;
         not_yet_listening: not listening

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_SERVER_SOCKET
   --  Accessors

   listening: BOOLEAN
      --  Listening for connections?

   local_address: STRING
      --  Which local address are we listening on? "All" is a default
      --  response.
      require
         listening: listening
      ensure
         not_void: Result /= Void;
         still_listening: listening;
         clone: equal(Result,local_address_rep) and Result /= local_address_rep

   local_port: INTEGER
      --  Which port are we listening on?
      require
         listening: listening
      ensure
         still_listening: listening

feature(s) from ES_SERVER_SOCKET
   get_next_connection
      --  Get the next available connection.
      require
         listening: listening
      ensure
         still_listening: listening;
         result_present: not error = remote_connection /= Void;
         result_open: remote_connection /= Void implies remote_connection.open and remote_connection.connected

   remote_connection: ES_STREAM_SOCKET
      --  Incomming connection

feature(s) from ES_SERVER_SOCKET
   --  Lifecycle

   start_listening (address: STRING; port: INTEGER)
      --  Set this socket to listen on address:port. address
      --  can be set to its default: "All".
      require
         open: open;
         not_yet_listening: not listening;
         not_void: address /= Void;
         valid_port: port >= 0 and port <= 65535
      ensure
         still_open: open;
         listening: not error = listening;
         correct_address: not error implies equal(local_address,address);
         correct_port: not error and port > 0 implies local_port = port;
         chosen_port: not error and port = 0 implies local_port > 0 and local_port <= 65535

invariant

    closed_is_not_open: closed = not open;

    only_listen_when_open: listening implies open;

end of ES_SERVER_SOCKET