Further contracts for non-Void-safe users

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/wsf_request_methods.e

@@ -421,7 +421,7 @@ feature {WSF_REQUEST_METHODS} -- Implementation
 	add_methods (lst: ITERABLE [READABLE_STRING_8])
 			-- Enable methods from `lst'.
 		require
-			lst_attached: lst /= Void
+			lst_all_attached: lst /= Void and then across lst as c all c.item /= Void end
 		do
 			if not is_locked then
 				across

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
+			-- URI 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