Added non-Void contracts for classes previously flagged by AutoTest

library/server/wsf/extension/wsf_resource_handler_helper.e

@@ -14,6 +14,9 @@ feature -- Execute template
 
 	execute_methods (req: WSF_REQUEST; res: WSF_RESPONSE)
 			-- Execute request and dispatch according to the request method.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		local
 			m: READABLE_STRING_8
 		do
@@ -43,6 +46,11 @@ feature -- Execute template
 feature -- Method Get
 
 	execute_get (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			get_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_get)
 		do
 			do_get (req, res)
 		end
@@ -52,9 +60,9 @@ feature -- Method Get
 			-- If the GET request is SUCCESS, we respond with
 			-- 200 OK, and a representation of the resource.
 			-- If the GET request is not SUCCESS, we response with
-			-- 404 Resource not found
+			-- 404 Resource not found.
 			-- If is a Condition GET and the resource does not change we send a
-			-- 304, Resource not modifed	
+			-- 304, Resource not modifed.
 		do
 			handle_not_implemented ("Method GET not implemented", req, res)
 		end
@@ -62,6 +70,11 @@ feature -- Method Get
 feature -- Method Post
 
 	execute_post (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			post_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_post)
 		do
 			if req.is_chunked_input then
 				do_post (req, res)
@@ -90,6 +103,11 @@ feature -- Method Post
 feature-- Method Put
 
 	execute_put (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			put_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_put)
 		do
 			if req.is_chunked_input then
 				do_put (req, res)
@@ -110,6 +128,11 @@ feature-- Method Put
 feature -- Method DELETE
 
 	execute_delete (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			delete_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_delete)
 		do
 			do_delete (req, res)
 		end
@@ -126,6 +149,11 @@ feature -- Method DELETE
 feature -- Method CONNECT
 
 	execute_connect (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			connect_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_connect)
 		do
 			do_connect (req, res)
 		end
@@ -138,6 +166,11 @@ feature -- Method CONNECT
 feature -- Method HEAD
 
 	execute_head (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			head_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_head)
 		do
 			do_head (req, res)
 		end
@@ -157,6 +190,11 @@ feature -- Method HEAD
 feature -- Method OPTIONS
 
 	execute_options (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			options_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_options)
 		do
 			do_options (req, res)
 		end
@@ -170,6 +208,11 @@ feature -- Method OPTIONS
 feature -- Method TRACE
 
 	execute_trace (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
+			trace_method: req.request_method.as_upper.same_string ({HTTP_REQUEST_METHODS}.method_trace)
 		do
 			do_trace (req, res)
 		end
@@ -183,20 +226,30 @@ feature -- Method TRACE
 feature -- Method Extension Method
 
 	execute_extension_method (req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Execute `req' responding into `res'.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			do_extension_method (req, res)
 		end
 
 	do_extension_method (req: WSF_REQUEST; res: WSF_RESPONSE)
+		-- Execute `req' responding into `res'.
+	require
+		req_attached: req /= Void
+		res_attached: res /= Void
 		do
 			handle_not_implemented ("Method extension-method not implemented", req, res)
 		end
 
 feature -- Retrieve content from WGI_INPUT_STREAM
 
-	retrieve_data  ( req : WSF_REQUEST) : STRING
+	retrieve_data  (req: WSF_REQUEST): STRING
-			-- retrieve the content from the input stream
+			-- Retrieve the content from the input stream.
-			-- handle differents transfers
+			-- Handle different transfers.
+		require
+			req_attached: req /= Void
 		do
 			create Result.make_empty
 			req.read_input_data_into (Result)
@@ -207,15 +260,22 @@ feature -- Handle responses
 	-- The option : Server-driven negotiation: uses request headers to select a variant
 	-- More info : http://www.w3.org/Protocols/rfc2616/rfc2616-sec12.html#sec12
 
---	supported_content_types: detachable ARRAY [READABLE_STRING_8]
+	--	supported_content_types: detachable ARRAY [READABLE_STRING_8]
---			-- Supported content types
+	--			-- Supported content types
---			-- Can be redefined
+	--			-- Can be redefined
---		do
+	--		do
---			Result := Void
+	--			Result := Void
---		end
+	--		end
+
+	-- TODO: review HTTP requirements on `a_description' for each individual error code.
 
 	handle_error (a_description: STRING; a_status_code: INTEGER; req: WSF_REQUEST; res: WSF_RESPONSE)
 			-- Handle an error.
+		require
+			a_description_attached: a_description /= Void
+			a_status_code_valid: a_status_code > 0
+			req_attached: req /= Void
+			res_attached: res /= Void
 		local
 			h: HTTP_HEADER
 		do
@@ -229,55 +289,99 @@ feature -- Handle responses
 		end
 
 	handle_not_implemented (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.not_implemented.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.not_implemented, req, res)
 		end
 
 	handle_bad_request_response (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.bad_request.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.bad_request, req, res)
 		end
 
 	handle_resource_not_found_response (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.not_found.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.not_found, req, res)
 		end
 
 	handle_forbidden (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
-			-- Handle forbidden.
+			-- Handle error {HTTP_STATUS_CODE}.forbidden.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.forbidden, req, res)
 		end
 
 feature -- Handle responses: others		
 
-	handle_precondition_fail_response (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE )
+	handle_precondition_fail_response (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.precondition_failed.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.precondition_failed, req, res)
 		end
 
-	handle_internal_server_error (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE )
+	handle_internal_server_error (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.internal_server_error.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.internal_server_error, req, res)
 		end
 
 	handle_method_not_allowed_response (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.method_not_allowed.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.method_not_allowed, req, res)
 		end
 
 	handle_resource_not_modified_response (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.not_modified.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.not_modified, req, res)
 		end
 
 	handle_resource_conflict_response (a_description: STRING; req: WSF_REQUEST; res: WSF_RESPONSE)
+			-- Handle error {HTTP_STATUS_CODE}.conflict.
+		require
+			a_description_attached: a_description /= Void
+			req_attached: req /= Void
+			res_attached: res /= Void
 		do
 			handle_error (a_description, {HTTP_STATUS_CODE}.conflict, req, res)
 		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_request_methods.e

@@ -55,17 +55,26 @@ feature {NONE} -- Initialization
 		end
 
 	make (n: INTEGER)
+			-- Initialize with space 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_attached: v /= Void
 		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,7 +419,9 @@ feature -- Access
 feature {WSF_REQUEST_METHODS} -- Implementation
 
 	add_methods (lst: ITERABLE [READABLE_STRING_8])
-			-- Enable methods from `lst'			
+			-- Enable methods from `lst'.
+		require
+			lst_attached: lst /= Void
 		do
 			if not is_locked then
 				across
@@ -418,7 +435,9 @@ 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
 		do
 			if v.is_case_insensitive_equal (method_get) then
 				enable_get
@@ -446,7 +465,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 +490,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'
+			-- Dispatch request `req' among  the `mappings'.
-			-- Set `is_dispatched' if the request were dispatched
+			-- 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
@@ -105,7 +134,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.
+			-- And return the associated handler (violating CQS) if mapping found and handler executed.
+		require
+			req_attached: req /= Void
+			res_attached: res /= Void
 		local
 			l_req_method: READABLE_STRING_8
 			head_res: WSF_HEAD_RESPONSE_WRAPPER
@@ -125,7 +157,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.
+			-- And return the associated handler (violating CQS) if mapping found and handler executed.
+		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 +187,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 +217,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 +250,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 +278,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 +339,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 +348,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 +357,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 +366,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 +375,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 +384,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 +395,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 +406,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 +416,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 +426,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 +436,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 +475,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 +485,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/src/wsf_head_response_wrapper.e

@@ -27,6 +27,9 @@ create
 feature {NONE} -- Initialization
 
 	make_from_response (res: WSF_RESPONSE)
+			-- Initialize from `res' (assumed to be a GET response).
+		require
+			res_attached: res /= Void
 		do
 			wsf_response := res
 			make_from_wgi (res.wgi_response)
@@ -65,10 +68,12 @@ feature -- Output operation
 		end
 
 invariant
+
 	transfered_content_length_is_zero: transfered_content_length = 0
+	wsf_response_attached: wsf_response /= 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