Third iteration of contracts for non-Void-safe users

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_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