indexing
	description: "Resources accessed over a network"
	status: "See note at end of class"
	date: "$Date$"
	revision: "$Revision$"

deferred class interface
	NETWORK_RESOURCE

feature -- Access

	address: NETWORK_RESOURCE_URL
			-- Address of URL

	bytes_transferred: INTEGER
			-- Number of transferred bytes

	Check_instruction: INTEGER is 7
			-- Exception code for violated check
			-- (from EXCEP_CONST)

	Class_invariant: INTEGER is 6
			-- Exception code for violated class invariant
			-- (from EXCEP_CONST)

	Com_exception: INTEGER is 28
			-- Exception code for a COM error.
			-- (from EXCEP_CONST)

	Developer_exception: INTEGER is 24
			-- Exception code for developer exception
			-- (from EXCEP_CONST)

	External_exception: INTEGER is 18
			-- Exception code for operating system error
			-- which does not set the errno variable
			-- (Unix-specific)
			-- (from EXCEP_CONST)

	Floating_point_exception: INTEGER is 5
			-- Exception code for floating point exception
			-- (from EXCEP_CONST)

	hash_code: INTEGER
			-- Hash function
			-- (from DATA_RESOURCE)
		ensure -- from HASHABLE
			good_hash_value: Result >= 0

	Incorrect_inspect_value: INTEGER is 9
			-- Exception code for inspect value which is not one
			-- of the inspect constants, if there is no Else_part
			-- (from EXCEP_CONST)

	Io_exception: INTEGER is 21
			-- Exception code for I/O error
			-- (from EXCEP_CONST)

	last_packet: STRING
			-- Last packet read
			-- (from DATA_RESOURCE)

	last_packet_size: INTEGER
			-- Size of last packet

	location: STRING
			-- Location of resource
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			address_exists: address /= void

	Loop_invariant: INTEGER is 11
			-- Exception code for violated loop invariant
			-- (from EXCEP_CONST)

	Loop_variant: INTEGER is 10
			-- Exception code for non-decreased loop variant
			-- (from EXCEP_CONST)

	mode: INTEGER
			-- Current mode
			-- (from DATA_RESOURCE)

	No_more_memory: INTEGER is 2
			-- Exception code for failed memory allocation
			-- (from EXCEP_CONST)

	Operating_system_exception: INTEGER is 22
			-- Exception code for operating system error
			-- which sets the errno variable
			-- (Unix-specific)
			-- (from EXCEP_CONST)

	port: INTEGER
			-- Port used by service
			-- (from DATA_RESOURCE)

	Postcondition: INTEGER is 4
			-- Exception code for violated postcondition
			-- (from EXCEP_CONST)

	Precondition: INTEGER is 3
			-- Exception code for violated precondition
			-- (from EXCEP_CONST)

	read_buffer_size: INTEGER
			-- Size of read buffer

	Rescue_exception: INTEGER is 14
			-- Exception code for exception in rescue clause
			-- (from EXCEP_CONST)

	Retrieve_exception: INTEGER is 23
			-- Exception code for retrieval error
			-- may be raised by retrieved in IO_MEDIUM.
			-- (from EXCEP_CONST)

	Routine_failure: INTEGER is 8
			-- Exception code for failed routine
			-- (from EXCEP_CONST)

	Runtime_io_exception: INTEGER is 27
			-- Exception code for I/O error raised by runtime functions
			-- such as store/retrieve, file access...
			-- (from EXCEP_CONST)

	service: STRING
			-- Name of service
			-- (from DATA_RESOURCE)

	Signal_exception: INTEGER is 12
			-- Exception code for operating system signal
			-- (from EXCEP_CONST)

	Void_assigned_to_expanded: INTEGER is 19
			-- Exception code for assignment of void value
			-- to expanded entity
			-- (from EXCEP_CONST)

	Void_call_target: INTEGER is 1
			-- Exception code for feature applied to void reference
			-- (from EXCEP_CONST)
	
feature -- Measurement

	count: INTEGER
			-- Size of data resource
			-- (from DATA_RESOURCE)
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is resource equal to other?
			-- (from DATA_RESOURCE)
		require -- from ANY
			other_not_void: other /= void
		ensure -- from ANY
			symmetric: Result implies other.is_equal (Current)
			consistent: standard_is_equal (other) implies Result
	
feature -- Status report

	address_exists: BOOLEAN
			-- Does address exists?

	assertion_violation: BOOLEAN
			-- Is last exception originally due to a violated
			-- assertion or non-decreasing variant?
			-- (from EXCEPTIONS)

	class_name: STRING
			-- Name of the class that includes the recipient
			-- of original form of last exception
			-- (from EXCEPTIONS)

	developer_exception_name: STRING
			-- Name of last developer-raised exception
			-- (from EXCEPTIONS)
		require -- from EXCEPTIONS
			applicable: is_developer_exception

	error: BOOLEAN
			-- Has an error occurred?
			-- (from DATA_RESOURCE)

	error_code: INTEGER
			-- Code of error
			-- (from DATA_RESOURCE)

	error_text (code: INTEGER): STRING
			-- Textual description of error
			-- (from DATA_RESOURCE_ERROR_CONSTANTS)
		require -- from DATA_RESOURCE_ERROR_CONSTANTS
			positive_code: code > 0

	exception: INTEGER
			-- Code of last exception that occurred
			-- (from EXCEPTIONS)

	exception_trace: STRING
			-- String representation of the exception trace
			-- (from EXCEPTIONS)

	has_packet: BOOLEAN
			-- Is there a packet available in last_packet?
			-- (from DATA_RESOURCE)

	is_count_valid: BOOLEAN
			-- Is value in count valid?

	is_developer_exception: BOOLEAN
			-- Is the last exception originally due to
			-- a developer exception?
			-- (from EXCEPTIONS)

	is_developer_exception_of_name (name: STRING): BOOLEAN
			-- Is the last exception originally due to a developer
			-- exception of name name?
			-- (from EXCEPTIONS)

	is_hashable: BOOLEAN
			-- Are objects of current type hashable?
			-- (from DATA_RESOURCE)
		ensure -- from HASHABLE
			ok_if_not_default: Result implies (Current /= default)

	is_mode_set: BOOLEAN
			-- Has resource mode been set?
			-- (from DATA_RESOURCE)

	is_open: BOOLEAN
			-- Is resource open?

	is_packet_pending: BOOLEAN
			-- Can another packet currently be read out?

	is_proxy_supported: BOOLEAN
			-- Is proxy supported by resource?
			-- (from DATA_RESOURCE)

	is_proxy_used: BOOLEAN
			-- Is a proxy used?

	is_readable: BOOLEAN
			-- Is it possible to open in read mode currently?
		ensure -- from DATA_RESOURCE
			mode_unchanged: mode = old mode

	is_signal: BOOLEAN
			-- Is last exception originally due to an external
			-- event (operating system signal)?
			-- (from EXCEPTIONS)

	is_system_exception: BOOLEAN
			-- Is last exception originally due to an
			-- external event (operating system error)?
			-- (from EXCEPTIONS)

	is_writable: BOOLEAN
			-- Is it possible to open in write mode currently?
		ensure -- from DATA_RESOURCE
			mode_unchanged: mode = old mode

	meaning (except: INTEGER): STRING
			-- A message in English describing what except is
			-- (from EXCEPTIONS)

	original_class_name: STRING
			-- Name of the class that includes the recipient
			-- of original form of last exception
			-- (from EXCEPTIONS)

	original_exception: INTEGER
			-- Original code of last exception that triggered
			-- current exception
			-- (from EXCEPTIONS)

	original_recipient_name: STRING
			-- Name of the routine whose execution was
			-- interrupted by original form of last exception
			-- (from EXCEPTIONS)

	original_tag_name: STRING
			-- Assertion tag for original form of last
			-- assertion violation.
			-- (from EXCEPTIONS)

	read_mode: BOOLEAN
			-- Is read mode set?
			-- (from DATA_RESOURCE)

	recipient_name: STRING
			-- Name of the routine whose execution was
			-- interrupted by last exception
			-- (from EXCEPTIONS)

	supports_multiple_transactions: BOOLEAN
			-- Does resource support multiple tranactions per connection?
			-- (from DATA_RESOURCE)

	tag_name: STRING
			-- Tag of last violated assertion clause
			-- (from EXCEPTIONS)

	timeout: INTEGER
			-- Connection timeout
			-- (from DATA_RESOURCE)

	transfer_initiated: BOOLEAN
			-- Has transfer being initiated.
			-- (from DATA_RESOURCE)

	valid_mode (n: INTEGER): BOOLEAN
			-- Is mode n valid?
			-- (from DATA_RESOURCE)

	write_mode: BOOLEAN
			-- Is write mode set?
			-- (from DATA_RESOURCE)
	
feature -- Status setting

	catch (code: INTEGER)
			-- Make sure that any exception of code code will be
			-- caught. This is the default.
			-- (from EXCEPTIONS)

	close
			-- Close.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			open: is_open
		ensure -- from DATA_RESOURCE
			closed: not is_open
			mode_unchanged: mode = old mode
			no_packet_available: not (has_packet and is_packet_pending)

	die (code: INTEGER)
			-- Terminate execution with exit status code,
			-- without triggering an exception.
			-- (from EXCEPTIONS)

	ignore (code: INTEGER)
			-- Make sure that any exception of code code will be
			-- ignored. This is not the default.
			-- (from EXCEPTIONS)

	initiate_transfer
			-- Initiate transfer.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			no_error_occurred: not error
			mode_set: is_mode_set
			open: is_open
			not_initiated: not transfer_initiated
		ensure -- from DATA_RESOURCE
			failure_means_error: not transfer_initiated implies error

	message_on_failure
			-- Print an exception history table
			-- in case of failure.
			-- This is the default.
			-- (from EXCEPTIONS)

	no_message_on_failure
			-- Do not print an exception history table
			-- in case of failure.
			-- (from EXCEPTIONS)

	open
			-- Open resource.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			no_error_occurred: not error
			mode_set: is_mode_set
		ensure -- from DATA_RESOURCE
			no_packet_available: not (has_packet and is_packet_pending)
			initiated_flag_reset: not transfer_initiated
			failure_means_error: not is_open implies error

	raise (name: STRING)
			-- Raise a developer exception of name name.
			-- (from EXCEPTIONS)

	reset_error
			-- Reset error.
			-- (from DATA_RESOURCE)
		ensure -- from DATA_RESOURCE
			error_reset: not error

	reset_proxy
			-- Reset proxy information.
			-- (from DATA_RESOURCE)
		ensure -- from DATA_RESOURCE
			proxy_reset: not address.is_proxy_used

	reuse_connection (other: DATA_RESOURCE)
			-- Reuse connection of other.
		require -- from DATA_RESOURCE
			other_exists: other /= void
			same_type: same_type (other)
			supports_multiple_transactions: supports_multiple_transactions and other.supports_multiple_transactions
			other_opened: other.is_open

	set_password (pw: STRING)
			-- Set password to pw.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			password_accepted: address.is_password_accepted
			non_empty_password: pw /= void and then not pw.is_empty

	set_port (port_no: INTEGER)
			-- Set port number to port_no.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			closed: not is_open
			non_negative_port_number: port_no >= 0
		ensure -- from DATA_RESOURCE
			port_set: port = port_no

	set_proxy (host: STRING; port_no: INTEGER)
			-- Set proxy host to host and port to port_no.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			proxy_supported: is_proxy_supported
			closed: not is_open
			non_empty_host: host /= void and then not host.is_empty
			host_ok: address.proxy_host_ok (host)
			non_negative_port: port_no >= 0
		ensure -- from DATA_RESOURCE
			proxy_set: address.is_proxy_used

	set_proxy_information (pi: PROXY_INFORMATION)
			-- Set proxy information to pi.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			proxy_supported: is_proxy_supported
		ensure -- from DATA_RESOURCE
			proxy_set: address.is_proxy_used

	set_read_buffer_size (n: INTEGER)
			-- Set size of read buffer.
		require -- from DATA_RESOURCE
			size_positive: n > 0
		ensure -- from DATA_RESOURCE
			buffer_size_set: read_buffer_size = n

	set_read_mode
			-- Set read mode.
			-- (from DATA_RESOURCE)
		ensure -- from DATA_RESOURCE
			read_mode_set: read_mode

	set_timeout (n: INTEGER)
			-- Set connection timeout to n.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			non_negative: n >= 0
		ensure -- from DATA_RESOURCE
			timeout_set: timeout = n

	set_username (un: STRING)
			-- Set username to un.
			-- (from DATA_RESOURCE)
		require -- from DATA_RESOURCE
			username_accepted: address.has_username
			non_empty_username: un /= void and then not un.is_empty

	set_write_mode
			-- Set write mode.
			-- (from DATA_RESOURCE)
		ensure -- from DATA_RESOURCE
			write_mode_set: write_mode
	
feature -- Removal

	dispose
			-- Clean up resource.
			-- (from DATA_RESOURCE)
	
feature -- Input

	read
			-- Read packet.
		require -- from DATA_RESOURCE
			no_error_occurred: not error
			open: is_open
			transfer_initated: transfer_initiated
			readable: is_readable
			positive_read_buffer_size: read_buffer_size > 0
			packet_pending: is_packet_pending
		ensure -- from DATA_RESOURCE
			packet_received: is_packet_pending implies last_packet_size > 0
			counter_correct: not error implies bytes_transferred = old bytes_transferred + last_packet_size
	
feature -- Output

	put (other: DATA_RESOURCE)
			-- Write out resource other.
		require -- from DATA_RESOURCE
			no_error_occurred: not (error and other.error)
			other_resource_exists: other /= void
			resources_open: is_open and other.is_open
			writable: is_writable
			transfer_initated: transfer_initiated
	
invariant

	main_socket_ok: (main_socket /= void and not error) implies main_socket.socket_ok
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from DATA_RESOURCE
	address_assigned: address /= void
	timeout_non_negative: timeout >= 0
	packet_constraint: not (has_packet xor last_packet /= void)
	pending_constraint: is_packet_pending implies (is_open and is_readable and transfer_initiated)
	error_definition: error = (error_code /= 0)
	valid_count_constraint: count > 0 implies is_count_valid
	mode_constraint: is_mode_set = read_mode xor write_mode

end -- class NETWORK_RESOURCE