Merge remote-tracking branch 'upstream/master' into cors

library/server/wsf/router/support/uri/wsf_uri_handler.e

@@ -15,6 +15,10 @@ inherit
 feature -- Execution
 
 	execute (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute handler for `req' and respond in `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		deferred
 		end
 
@@ -26,7 +30,7 @@ feature {WSF_ROUTER} -- Mapping
 		end
 
 note
-	copyright: "2011-2012, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
+	copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
 	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software

library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_routed_service.e

@@ -13,11 +13,19 @@ inherit
 feature -- Mapping helper: uri
 
 	map_uri_template (a_tpl: STRING; h: WSF_URI_TEMPLATE_HANDLER)
+			-- Map `h' as handler for `a_tpl'
+		require
+			a_tpl_attached: a_tpl /= Void
+			h_attached: h /= Void	
 		do
 			map_uri_template_with_request_methods (a_tpl, h, Void)
 		end
 
 	map_uri_template_with_request_methods (a_tpl: READABLE_STRING_8; h: WSF_URI_TEMPLATE_HANDLER; rqst_methods: detachable WSF_REQUEST_METHODS)
+			-- Map `h' as handler for `a_tpl' for request methods `rqst_methods'.
+		require
+			a_tpl_attached: a_tpl /= Void
+			h_attached: h /= Void
 		do
 			router.map_with_request_methods (create {WSF_URI_TEMPLATE_MAPPING}.make (a_tpl, h), rqst_methods)
 		end
@@ -25,17 +33,25 @@ feature -- Mapping helper: uri
 feature -- Mapping helper: uri agent
 
 	map_uri_template_agent (a_tpl: READABLE_STRING_8; proc: PROCEDURE [ANY, TUPLE [req: WSF_REQUEST; res: WSF_RESPONSE]])
+			-- Map `proc' as handler for `a_tpl'
+		require
+			a_tpl_attached: a_tpl /= Void
+			proc_attached: proc /= Void	
 		do
 			map_uri_template_agent_with_request_methods (a_tpl, proc, Void)
 		end
 
 	map_uri_template_agent_with_request_methods (a_tpl: READABLE_STRING_8; proc: PROCEDURE [ANY, TUPLE [req: WSF_REQUEST; res: WSF_RESPONSE]]; rqst_methods: detachable WSF_REQUEST_METHODS)
+			-- Map `proc' as handler for `a_tpl' for request methods `rqst_methods'.
+		require
+			a_tpl_attached: a_tpl /= Void
+			proc_attached: proc /= Void
 		do
 			map_uri_template_with_request_methods (a_tpl, create {WSF_URI_TEMPLATE_AGENT_HANDLER}.make (proc), rqst_methods)
 		end
 
 note
-	copyright: "2011-2012, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
+	copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
 	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software

library/server/wsf/router/support/uri_template/wsf_uri_template_handler.e

@@ -15,6 +15,10 @@ inherit
 feature -- Execution
 
 	execute (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding in `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		deferred
 		end
 

library/server/wsf/router/support/uri_template/wsf_uri_template_mapping.e

@@ -21,17 +21,25 @@ feature -- Access
 feature -- Change
 
 	set_handler	(h: like handler)
+			-- <Precursor>
 		do
 			handler := h
+		ensure then
+			h_aliased: handler = h
 		end
 
 feature {NONE} -- Execution
 
 	execute_handler (h: like handler; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- <Precursor>
 		do
 			h.execute (req, res)
 		end
 
+invariant
+
+	handler_attached: handler /= Void
+
 note
 	copyright: "2011-2012, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
 	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"

library/server/wsf/router/support/uri_template/wsf_uri_template_mapping_i.e

@@ -15,20 +15,27 @@ inherit
 feature {NONE} -- Initialization
 
 	make (s: READABLE_STRING_8; h: like handler)
+			-- <Precursor>
 		do
 			make_from_template (create {URI_TEMPLATE}.make (s), h)
 		end
 
 	make_from_template (tpl: URI_TEMPLATE; h: like handler)
+			-- Create with `h' as the handler for resources matching `tpl'
+		require
+			tpl_attached: tpl /= Void
+			h_attached: h /= Void	
 		do
 			template := tpl
 			set_handler (h)
+		ensure
+			tpl_aliased: template = tpl
 		end
 
 feature -- Access		
 
 	associated_resource: READABLE_STRING_8
-			-- Associated resource
+			-- URI template text of handled resource
 		do
 			Result := template.template
 		end
@@ -38,6 +45,9 @@ feature -- Access
 feature -- Change
 
 	set_handler (h: like handler)
+			-- Set `handler' to `h'.
+		require
+			h_attached: h /= Void
 		deferred
 		end
 
@@ -59,6 +69,7 @@ feature -- Status
 		end
 
 	routed_handler (req: WSF_REQUEST; res: WSF_RESPONSE; a_router: WSF_ROUTER): detachable WSF_HANDLER
+			-- <Precursor>
 		local
 			tpl: URI_TEMPLATE
 			p: READABLE_STRING_32
@@ -88,13 +99,21 @@ feature -- Status
 feature {NONE} -- Execution
 
 	execute_handler (h: like handler; req: WSF_REQUEST; res: WSF_RESPONSE)
-			-- Execute handler `h' with `req' and `res' for Current mapping
+			-- Run `h' to execute `req' responding in `res'.
+		require
+			h_attached: h /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		deferred
 		end
 
 feature {NONE} -- Implementation
 
 	based_uri_template (a_tpl: like template; a_router: WSF_ROUTER): like template
+			-- Version of `a_tpl' using bas URI of `a_router'
+		require
+			a_tpl_attached: a_tpl /= Void
+			a_router_attached: a_router /= Void
 		do
 			if attached a_router.base_url as l_base_url then
 				Result := a_tpl.duplicate
@@ -102,6 +121,8 @@ feature {NONE} -- Implementation
 			else
 				Result := a_tpl
 			end
+		ensure
+			based_uri_template_attached: Result /= Void
 		end
 
 note

library/server/wsf/router/wsf_request_methods.e

@@ -55,17 +55,26 @@ feature {NONE} -- Initialization
 		end
 
 	make (n: INTEGER)
+			-- Initialize with capacity for `n' methods.
+		require
+			valid_number_of_items: n >= 0
 		do
 			create methods.make (n)
 		end
 
 	make_from_iterable (v: ITERABLE [READABLE_STRING_8])
+			-- Initialize for all methods named by `v'.
+		require
+			v_all_methods_attached: v /= Void and then across v as c all c.item /= Void end
 		do
 			make (1)
 			add_methods (v)
 		end
 
 	make_from_string (v: READABLE_STRING_8)
+			-- Initialize from comma-separated methods named in `v'.
+		require
+			v_attached: v /= Void
 		do
 			make_from_iterable (v.split (','))
 		end
@@ -83,6 +92,7 @@ feature -- Status report
 	has (a_method: READABLE_STRING_8): BOOLEAN
 			-- Has `a_method' enabled?
 		require
+			a_method_attached: a_method /= Void
 			a_method_is_uppercase: a_method.same_string (a_method.as_upper)
 		do
 			-- First look for string object itself,
@@ -95,67 +105,71 @@ feature -- Status report
 		end
 
 	has_some_of (a_methods: WSF_REQUEST_METHODS): BOOLEAN
-			-- Has any methods from `a_methods' enabled?
+			-- Have any methods from `a_methods' been enabled?
+		require
+			a_methods_attached: a_methods /= Void
 		do
 			Result := across a_methods as c some has (c.item) end
 		end
 
 	has_all_of (a_methods: WSF_REQUEST_METHODS): BOOLEAN
-			-- Has all methods from `a_methods' enabled?
+			-- Have all methods from `a_methods' been enabled?
+		require
+			a_methods_attached: a_methods /= Void
 		do
 			Result := across a_methods as c all has (c.item) end
 		end
 
 	has_method_get: BOOLEAN
-			-- Has method GET enabled?
+			-- Has method GET been enabled?
 		do
 			Result := has (method_get)
 		end
 
 	has_method_post: BOOLEAN
-			-- Has method POST enabled?
+			-- Has method POST been enabled?
 		do
 			Result := has (method_post)
 		end
 
 	has_method_put: BOOLEAN
-			-- Has method PUT enabled?
+			-- Has method PUT been enabled?
 		do
 			Result := has (method_put)
 		end
 
 	has_method_delete: BOOLEAN
-			-- Has method DELETE enabled?
+			-- Has method DELETE been enabled?
 		do
 			Result := has (method_delete)
 		end
 
 	has_method_options: BOOLEAN
-			-- Has method OPTIONS enabled?
+			-- Has method OPTIONS been enabled?
 		do
 			Result := has (method_options)
 		end
 
 	has_method_head: BOOLEAN
-			-- Has method HEAD enabled?
+			-- Has method HEAD been enabled?
 		do
 			Result := has (method_head)
 		end
 
 	has_method_trace: BOOLEAN
-			-- Has method TRACE enabled?
+			-- Has method TRACE been enabled?
 		do
 			Result := has (method_trace)
 		end
 
 	has_method_connect: BOOLEAN
-			-- Has method CONNECT enabled?
+			-- Has method CONNECT been enabled?
 		do
 			Result := has (method_connect)
 		end
 
 	has_method_patch: BOOLEAN
-			-- Has method PATCH enabled?
+			-- Has method PATCH been enabled?
 		do
 			Result := has (method_patch)
 		end
@@ -384,6 +398,7 @@ feature -- Element change
 	disable_custom (m: READABLE_STRING_8)
 		require
 			is_not_locked: not is_locked
+			m_attached: m /= Void
 			not_blank: not across m as mc some mc.item.is_space end
 			custom_enabled: has (m.as_upper)
 		do
@@ -404,13 +419,17 @@ feature -- Access
 feature {WSF_REQUEST_METHODS} -- Implementation
 
 	add_methods (lst: ITERABLE [READABLE_STRING_8])
-			-- Enable methods from `lst'			
+			-- Enable methods from `lst'.
+		require
+			lst_all_attached: lst /= Void and then across lst as c all c.item /= Void end
 		do
 			if not is_locked then
 				across
 					lst as c
 				loop
-					add_method_using_constant (c.item)
+					if not c.item.is_empty and not has (c.item) then
+						add_method_using_constant (c.item)
+					end
 				end
 			end
 		end
@@ -418,7 +437,11 @@ feature {WSF_REQUEST_METHODS} -- Implementation
 feature {NONE} -- Implementation		
 
 	add_method_using_constant (v: READABLE_STRING_8)
-			-- Add method `v' using method_* constant
+			-- Add method `v' using method_* constant.
+		require
+			v_attached: v /= Void
+			v_not_empty: not v.is_empty
+			new_method: not has (v)
 		do
 			if v.is_case_insensitive_equal (method_get) then
 				enable_get
@@ -446,7 +469,10 @@ feature {NONE} -- Implementation
 		end
 
 	prune_method (v: READABLE_STRING_8)
+			-- Remove method named `v' from `Current'.
+			-- Does nothing if `Current' `is_locked'.
 		require
+			v_attached: v /= Void
 			is_upper_case: v.same_string (v.as_upper)
 		local
 			m: READABLE_STRING_8
@@ -468,10 +494,12 @@ feature {NONE} -- Implementation
 		end
 
 invariant
+
+	methods_attached: methods /= Void
 	methods_are_uppercase: across methods as c all c.item.same_string (c.item.as_upper) end
 
 ;note
-	copyright: "2011-2012, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
+	copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
 	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software

library/server/wsf/router/wsf_routed_service.e

@@ -36,7 +36,10 @@ feature -- Execution
 
 	execute (req: WSF_REQUEST; res: WSF_RESPONSE)
 			-- Dispatch the request
-			-- and if you dispatch is found, execute the default procedure `execute_default'
+			-- and if handler is not found, execute the default procedure `execute_default'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			if attached router.dispatch_and_return_handler (req, res) as p then
 				-- executed
@@ -46,7 +49,10 @@ feature -- Execution
 		end
 
 	execute_default (req: WSF_REQUEST; res: WSF_RESPONSE)
-			-- Default procedure
+			-- Dispatch requests without a matching handler.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		local
 			msg: WSF_DEFAULT_ROUTER_RESPONSE
 		do
@@ -62,7 +68,7 @@ feature -- Access
 			-- and associated request methods
 
 ;note
-	copyright: "2011-2012, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
+	copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
 	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software

library/server/wsf/router/wsf_router.e

@@ -23,26 +23,40 @@ create
 feature {NONE} -- Initialization
 
 	make (n: INTEGER)
-			-- Create the router with a capacity of `n' mappings
+			-- Create the router with a capacity of `n' mappings.
+		require
+			valid_number_of_items: n >= 0
 		do
-			create mappings.make (n)
 			initialize (n)
+		ensure
+			no_handler_set: count = 0
 		end
 
 	make_with_base_url (n: INTEGER; a_base_url: like base_url)
 			-- Make router allocated for at least `n' maps,
 			-- and use `a_base_url' as `base_url'
 			--| This avoids prefixing all the resource string.
+		require
+			valid_number_of_items: n >= 0
+			a_valid_base_url: (a_base_url /= Void and then a_base_url.is_empty) implies (a_base_url.starts_with ("/") and not a_base_url.ends_with ("/"))
 		do
 			make (n)
+			check
+				no_handler_set: count = 0
+					-- ensured by `make'
+			end
 			set_base_url (a_base_url)
 		end
 
 	initialize (n: INTEGER)
-			-- Initialize router
+			-- Initialize router.
+		require
+			valid_number_of_items: n >= 0
 		do
 			create mappings.make (n)
 			create pre_execution_actions
+		ensure
+			no_handler_set: count = 0
 		end
 
 	mappings: ARRAYED_LIST [WSF_ROUTER_ITEM]
@@ -51,13 +65,17 @@ feature {NONE} -- Initialization
 feature -- Mapping
 
 	map (a_mapping: WSF_ROUTER_MAPPING)
-			-- Map `a_mapping'
+			-- Map `a_mapping'.
+		require
+			a_mapping_attached: a_mapping /= Void
 		do
 			map_with_request_methods (a_mapping, Void)
 		end
 
 	map_with_request_methods (a_mapping: WSF_ROUTER_MAPPING; rqst_methods: detachable WSF_REQUEST_METHODS)
-			-- Map `a_mapping' for request methods `rqst_methods'
+			-- Map `a_mapping' for request methods `rqst_methods'.
+		require
+			a_mapping_attached: a_mapping /= Void
 		do
 			debug ("router")
 				-- Display conflict in mapping
@@ -76,7 +94,10 @@ feature -- Mapping
 feature -- Mapping handler
 
 	handle (a_resource: READABLE_STRING_8; f: WSF_ROUTER_MAPPING_FACTORY)
-			-- Map the mapping created by factory `f' for resource `a_resource'
+			-- Map the mapping created by factory `f' for resource `a_resource'.
+		require
+			a_resource_attached: a_resource /= Void
+			f_attached: f /= Void
 		do
 			handle_with_request_methods (a_resource, f, Void)
 		end
@@ -84,6 +105,9 @@ feature -- Mapping handler
 	handle_with_request_methods (a_resource: READABLE_STRING_8; f: WSF_ROUTER_MAPPING_FACTORY; rqst_methods: detachable WSF_REQUEST_METHODS)
 			-- Map the mapping created by factory `f' for resource `a_resource'	
 			-- and only for request methods `rqst_methods'
+		require
+			a_resource_attached: a_resource /= Void
+			f_attached: f /= Void
 		do
 			map_with_request_methods (f.new_mapping (a_resource), rqst_methods)
 		end
@@ -94,9 +118,14 @@ feature -- Access
 			-- `dispatch' set `is_dispatched' to True
 			-- if mapping was found, and associated handler executed
 
+feature -- Basic operations
+
 	dispatch (req: WSF_REQUEST; res: WSF_RESPONSE)
-			-- Dispatch request `req' among  the `mappings'
-			-- Set `is_dispatched' if the request were dispatched
+			-- Dispatch request `req' among  the `mappings'.
+			-- Set `is_dispatched' if the request were dispatched.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			if attached dispatch_and_return_handler (req, res) then
 				check is_dispatched: is_dispatched end
@@ -106,6 +135,10 @@ feature -- Access
 	dispatch_and_return_handler (req: WSF_REQUEST; res: WSF_RESPONSE): detachable WSF_HANDLER
 			-- Dispatch request `req' among the `mappings'
 			-- And return the associated handler if mapping found and handler executed.
+			--| Violates CQS
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		local
 			l_req_method: READABLE_STRING_8
 			head_res: WSF_HEAD_RESPONSE_WRAPPER
@@ -126,6 +159,11 @@ feature {NONE} -- Dispatch implementation
 	dispatch_and_return_handler_for_request_method (req: WSF_REQUEST; res: WSF_RESPONSE; a_request_method: READABLE_STRING_8): detachable WSF_HANDLER
 			-- Dispatch request `req' among the `mappings'
 			-- And return the associated handler if mapping found and handler executed.
+			--| Violates CQS
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			a_request_method_attached: a_request_method /= Void
 		local
 			m: WSF_ROUTER_MAPPING
 		do
@@ -151,6 +189,9 @@ feature {NONE} -- Dispatch implementation
 feature -- Status report
 
 	has_item_associated_with_resource (a_resource: READABLE_STRING_8; rqst_methods: detachable WSF_REQUEST_METHODS): BOOLEAN
+			-- Is there a handler for `a_resource' (taking into account `rqst_methods')?
+		require
+			a_resource_attached: a_resource /= Void
 		local
 			m: WSF_ROUTER_MAPPING
 			ok: BOOLEAN
@@ -178,6 +219,9 @@ feature -- Status report
 		end
 
 	item_associated_with_resource (a_resource: READABLE_STRING_8; rqst_methods: detachable WSF_REQUEST_METHODS): detachable WSF_ROUTER_ITEM
+			-- Handler and request methods for `a_resource', taking into account `rqst_methods'
+		require
+			a_resource_attached: a_resource /= Void
 		local
 			m: WSF_ROUTER_MAPPING
 			ok: BOOLEAN
@@ -208,6 +252,8 @@ feature -- Status report
 
 	allowed_methods_for_request (req: WSF_REQUEST): WSF_REQUEST_METHODS
 			-- Allowed methods for `req'
+		require
+			req_attched: req /= Void
 		local
 			m: WSF_ROUTER_MAPPING
 			l_rqsmethods: detachable WSF_REQUEST_METHODS
@@ -234,14 +280,18 @@ feature -- Status report
 feature -- Hook
 
 	execute_before (a_mapping: WSF_ROUTER_MAPPING)
-			-- Execute before the handler associated with the matching mapping is executed
+			-- Execute before the handler associated with `a_mapping' is executed.
+		require
+			a_mapping_attached: a_mapping /= Void
 		do
 			pre_execution_actions.call ([a_mapping])
 		end
 
 	execute_after (a_mapping: WSF_ROUTER_MAPPING)
-			-- Execute after the handler associated with the matching mapping is executed	
+			-- Execute after the handler associated with `a_mapping' is executed.
 			--| Could be redefined to add specific hook.
+		require
+			a_mapping_attached: a_mapping /= Void
 		do
 		end
 
@@ -291,6 +341,8 @@ feature -- Request methods helper
 			create Result
 			Result.enable_head
 			Result.lock
+		ensure
+			methods_head_not_void: Result /= Void
 		end
 
 	methods_options: WSF_REQUEST_METHODS
@@ -298,6 +350,8 @@ feature -- Request methods helper
 			create Result
 			Result.enable_options
 			Result.lock
+		ensure
+			methods_options_not_void: Result /= Void
 		end
 
 	methods_get: WSF_REQUEST_METHODS
@@ -305,6 +359,8 @@ feature -- Request methods helper
 			create Result
 			Result.enable_get
 			Result.lock
+		ensure
+			methods_get_not_void: Result /= Void
 		end
 
 	methods_post: WSF_REQUEST_METHODS
@@ -312,6 +368,8 @@ feature -- Request methods helper
 			create Result
 			Result.enable_post
 			Result.lock
+		ensure
+			methods_post_not_void: Result /= Void
 		end
 
 	methods_put: WSF_REQUEST_METHODS
@@ -319,6 +377,8 @@ feature -- Request methods helper
 			create Result
 			Result.enable_put
 			Result.lock
+		ensure
+			methods_put_not_void: Result /= Void
 		end
 
 	methods_delete: WSF_REQUEST_METHODS
@@ -326,6 +386,8 @@ feature -- Request methods helper
 			create Result
 			Result.enable_delete
 			Result.lock
+		ensure
+			methods_delete_not_void: Result /= Void
 		end
 
 	methods_head_get_post: WSF_REQUEST_METHODS
@@ -335,6 +397,8 @@ feature -- Request methods helper
 			Result.enable_get
 			Result.enable_post
 			Result.lock
+		ensure
+			methods_head_get_post_not_void: Result /= Void
 		end
 
 	methods_get_put_delete: WSF_REQUEST_METHODS
@@ -344,6 +408,8 @@ feature -- Request methods helper
 			Result.enable_put
 			Result.enable_delete
 			Result.lock
+		ensure
+			methods_get_put_not_void: Result /= Void
 		end
 
 	methods_head_get: WSF_REQUEST_METHODS
@@ -352,6 +418,8 @@ feature -- Request methods helper
 			Result.enable_head
 			Result.enable_get
 			Result.lock
+		ensure
+			methods_head_get_not_void: Result /= Void
 		end
 
 	methods_get_post: WSF_REQUEST_METHODS
@@ -360,6 +428,8 @@ feature -- Request methods helper
 			Result.enable_get
 			Result.enable_post
 			Result.lock
+		ensure
+			methods_get_post_not_void: Result /= Void
 		end
 
 	methods_put_post: WSF_REQUEST_METHODS
@@ -368,12 +438,16 @@ feature -- Request methods helper
 			Result.enable_put
 			Result.enable_post
 			Result.lock
+		ensure
+			methods_put_post_not_void: Result /= Void
 		end
 
 feature {NONE} -- Access: Implementation
 
 	request_method (req: WSF_REQUEST): READABLE_STRING_8
-			-- Request method from `req' to be used in the router implementation.
+			-- Request method from `req' to be used in the router implementation
+		require
+			req_attached: req /= Void
 		local
 			m: READABLE_STRING_8
 		do
@@ -403,6 +477,8 @@ feature {NONE} -- Access: Implementation
 
 	is_matching_request_methods (a_request_method: READABLE_STRING_8; a_rqst_methods: detachable WSF_REQUEST_METHODS): BOOLEAN
 			-- `a_request_method' is matching `a_rqst_methods' contents
+		require
+			a_request_method_attached: a_request_method /= Void
 		do
 			if a_rqst_methods /= Void and then not a_rqst_methods.is_empty then
 				Result := a_rqst_methods.has (a_request_method)
@@ -411,8 +487,13 @@ feature {NONE} -- Access: Implementation
 			end
 		end
 
+invariant
+
+	mappings_attached: mappings /= Void
+	pre_execution_actions_attached: pre_execution_actions /= Void
+
 note
-	copyright: "2011-2012, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
+	copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
 	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software

library/server/wsf/router/wsf_router_mapping.e

@@ -13,27 +13,36 @@ inherit
 feature {NONE} -- Initialization
 
 	make (a_resource: READABLE_STRING_8; h: like handler)
-			-- Create mapping based on resource `a_resource' and handler `h'
+			-- Create mapping based on resource `a_resource' and handler `h'.
+		require
+			a_resource_attached: a_resource /= Void
+			h_attached: h /= Void
 		deferred
 		end
 
 feature -- Access
 
 	associated_resource: READABLE_STRING_8
-			-- Associated resource
+			-- Name (URI, or URI template or regular expression or ...) of handled resource
 		deferred
+		ensure
+			assciated_resource_not_void: Result /= Void
 		end
 
 	handler: WSF_HANDLER
-			-- Handler associated with Current mapping.
+			-- Handler associated with `Current' mapping
 		deferred
+		ensure
+			handler_attached: Result /= Void
 		end
 
 feature -- Documentation
 
 	description: READABLE_STRING_32
-			-- Short description of associated mapping.
+			-- Short description of associated mapping
 		deferred
+		ensure
+			description_attached: Result /= Void
 		end
 
 feature -- Status report
@@ -47,25 +56,36 @@ feature -- Status report
 feature -- Status
 
 	is_mapping (req: WSF_REQUEST; a_router: WSF_ROUTER): BOOLEAN
-			-- Does Current accept `req'?
+			-- Does `Current' accept `req' when using `a_router'?
+		require
+			req_attached: req /= Void
+			a_router_attached: a_router /= Void
 		deferred
 		end
 
 	routed_handler (req: WSF_REQUEST; res: WSF_RESPONSE; a_router: WSF_ROUTER): detachable WSF_HANDLER
-			-- Return the handler if Current matches the request `req'.
+			-- Handler when `Current' matches the request `req'
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			a_router_attached: a_router /= Void
 		deferred
 		end
 
 feature -- Helper
 
 	path_from_request (req: WSF_REQUEST): READABLE_STRING_32
-			-- Path used by Current to check that Current mapping matches request `req'.
+			-- Path used by `Current' to check that mapping matches request `req'
+		require
+			req_attached: req /= Void
 		do
 			Result := req.path_info
+		ensure
+			path_from_request_attached: Result /= Void
 		end
 
 note
-	copyright: "2011-2012, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
+	copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others"
 	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software

library/server/wsf/router/wsf_router_mapping_factory.e

@@ -14,6 +14,8 @@ feature {WSF_ROUTER} -- Mapping
 
 	new_mapping (a_uri: READABLE_STRING_8): WSF_ROUTER_MAPPING
 			-- New mapping object
+		require
+			a_uri_attached: a_uri /= Void
 		deferred
 		ensure
 			Result_attached: Result /= Void