From ca5619c6fc58c1e1bab40a96d8d27b23ca68bce2 Mon Sep 17 00:00:00 2001 From: Colin Adams Date: Thu, 14 Mar 2013 11:48:46 +0000 Subject: [PATCH] Added non-Void contracts for classes previously flagged by AutoTest --- .../extension/wsf_resource_handler_helper.e | 134 ++++++++++++++++-- .../server/wsf/router/wsf_request_methods.e | 52 +++++-- .../server/wsf/router/wsf_routed_service.e | 12 +- library/server/wsf/router/wsf_router.e | 107 ++++++++++++-- .../wsf/src/wsf_head_response_wrapper.e | 7 +- 5 files changed, 265 insertions(+), 47 deletions(-) diff --git a/library/server/wsf/extension/wsf_resource_handler_helper.e b/library/server/wsf/extension/wsf_resource_handler_helper.e index cb676bb1..5d93c9a7 100644 --- a/library/server/wsf/extension/wsf_resource_handler_helper.e +++ b/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 the content from the input stream - -- handle differents transfers + retrieve_data (req: WSF_REQUEST): STRING + -- Retrieve the content from the input stream. + -- 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 --- -- Can be redefined --- do --- Result := Void --- end + -- supported_content_types: detachable ARRAY [READABLE_STRING_8] + -- -- Supported content types + -- -- Can be redefined + -- do + -- Result := Void + -- 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 diff --git a/library/server/wsf/router/wsf_request_methods.e b/library/server/wsf/router/wsf_request_methods.e index a2af35c3..a463425e 100644 --- a/library/server/wsf/router/wsf_request_methods.e +++ b/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 diff --git a/library/server/wsf/router/wsf_routed_service.e b/library/server/wsf/router/wsf_routed_service.e index a91d45a9..5f2c3499 100644 --- a/library/server/wsf/router/wsf_routed_service.e +++ b/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 diff --git a/library/server/wsf/router/wsf_router.e b/library/server/wsf/router/wsf_router.e index f25c8578..3612fec3 100644 --- a/library/server/wsf/router/wsf_router.e +++ b/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 @@ -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 diff --git a/library/server/wsf/src/wsf_head_response_wrapper.e b/library/server/wsf/src/wsf_head_response_wrapper.e index 4575b317..fa894143 100644 --- a/library/server/wsf/src/wsf_head_response_wrapper.e +++ b/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