From a3037832048fba199f1812b6471dcf1171ca4648 Mon Sep 17 00:00:00 2001 From: Colin Adams Date: Fri, 15 Mar 2013 14:06:37 +0000 Subject: [PATCH 1/2] Fifth round of contracts for non-Void-safe users --- .../wsf/extension/wsf_method_handlers.e | 7 +++++- .../starts_with/wsf_starts_with_handler.e | 7 ++++++ .../starts_with/wsf_starts_with_mapping_i.e | 24 +++++++++++++++++-- 3 files changed, 35 insertions(+), 3 deletions(-) diff --git a/library/server/wsf/extension/wsf_method_handlers.e b/library/server/wsf/extension/wsf_method_handlers.e index 06e828c1..b786a31e 100644 --- a/library/server/wsf/extension/wsf_method_handlers.e +++ b/library/server/wsf/extension/wsf_method_handlers.e @@ -24,7 +24,12 @@ inherit WSF_METHOD_HANDLER rename - do_method as do_put + do_method as do_post + end + + WSF_METHOD_HANDLER + rename + do_method as do_delete end WSF_METHOD_HANDLER diff --git a/library/server/wsf/router/support/starts_with/wsf_starts_with_handler.e b/library/server/wsf/router/support/starts_with/wsf_starts_with_handler.e index 98621841..b1d6d422 100644 --- a/library/server/wsf/router/support/starts_with/wsf_starts_with_handler.e +++ b/library/server/wsf/router/support/starts_with/wsf_starts_with_handler.e @@ -15,12 +15,19 @@ inherit feature -- Execution execute (a_start_path: READABLE_STRING_8; req: WSF_REQUEST; res: WSF_RESPONSE) + -- Handle `req' responding into `res'. + require + a_start_path_attached: a_start_path /= Void + req_attached: req /= Void + res_attached: res /= Void + path_start_with_a_start_path: req.path_info.starts_with (a_start_path) deferred end feature {WSF_ROUTER} -- Mapping new_mapping (a_uri: READABLE_STRING_8): WSF_ROUTER_MAPPING + -- do create {WSF_STARTS_WITH_MAPPING} Result.make (a_uri, Current) end diff --git a/library/server/wsf/router/support/starts_with/wsf_starts_with_mapping_i.e b/library/server/wsf/router/support/starts_with/wsf_starts_with_mapping_i.e index 6346e9dc..7618171c 100644 --- a/library/server/wsf/router/support/starts_with/wsf_starts_with_mapping_i.e +++ b/library/server/wsf/router/support/starts_with/wsf_starts_with_mapping_i.e @@ -33,7 +33,12 @@ feature -- Access feature -- Change set_handler (h: like handler) + -- Set `handler' to `h'. + require + h_attached: h /= Void deferred + ensure + h_aliased: handler = h end feature -- Documentation @@ -72,14 +77,23 @@ feature -- Status feature {NONE} -- Execution execute_handler (h: like handler; a_start_path: like uri; req: WSF_REQUEST; res: WSF_RESPONSE) - -- Execute handler `h' with `req' and `res' for Current mapping + -- Execute handler `h' with `req' and `res' for Current mapping. + require + h_attached: h /= Void + a_start_path_attached: a_start_path /= Void + req_attached: req /= Void + res_attached: res /= Void + path_start_with_a_start_path: req.path_info.starts_with (a_start_path) deferred end feature {NONE} -- Implementation based_uri (a_uri: like uri; a_router: WSF_ROUTER): like uri - -- `uri' prefixed by the `WSF_ROUTER.base_url' if any + -- `a_uri' prefixed by the `WSF_ROUTER.base_url' if any + require + a_uri_attached: a_uri /= Void + a_router_attached: a_router /= Void local s: STRING_8 do @@ -90,8 +104,14 @@ feature {NONE} -- Implementation else Result := a_uri end + ensure + based_uri_attached: Result /= Void end +invariant + + uri_attached: uri /= 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)" From 2d439a24145f500a0e1af230c1bb0dbdff36661d Mon Sep 17 00:00:00 2001 From: Colin Adams Date: Fri, 15 Mar 2013 14:50:59 +0000 Subject: [PATCH 2/2] Sixth round of contracts for non-Void-safe users --- .../wsf_router_self_documentation_handler.e | 18 ++++++++++++++++++ .../wsf_self_documented_handler.e | 5 +++++ library/server/wsf/router/wsf_handler.e | 4 ++++ 3 files changed, 27 insertions(+) diff --git a/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e b/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e index b0fbb6da..8ab6c2ab 100644 --- a/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e +++ b/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e @@ -26,14 +26,27 @@ create feature {NONE} -- Initialization make (a_router: WSF_ROUTER) + -- Initialize `router'. + require + a_router_attached: a_router /= Void do router := a_router + ensure + router_aliased: router = a_router + not_hidden: not is_hidden end make_hidden (a_router: WSF_ROUTER) + -- Initialize `router'. + -- Do not display documentation for `a_router'. + require + a_router_attached: a_router /= Void do make (a_router) is_hidden := True + ensure + router_aliased: router = a_router + hidden: is_hidden end router: WSF_ROUTER @@ -46,6 +59,7 @@ feature {NONE} -- Initialization feature -- Documentation mapping_documentation (m: WSF_ROUTER_MAPPING; a_request_methods: detachable WSF_REQUEST_METHODS): WSF_ROUTER_MAPPING_DOCUMENTATION + -- do create Result.make (m) Result.set_is_hidden (is_hidden) @@ -76,4 +90,8 @@ feature -- Execution res.send (m) end +invariant + + router_attached: router /= Void + end diff --git a/library/server/wsf/router/documentation/wsf_self_documented_handler.e b/library/server/wsf/router/documentation/wsf_self_documented_handler.e index 453ee958..ecc23695 100644 --- a/library/server/wsf/router/documentation/wsf_self_documented_handler.e +++ b/library/server/wsf/router/documentation/wsf_self_documented_handler.e @@ -12,7 +12,12 @@ feature -- Documentation mapping_documentation (m: WSF_ROUTER_MAPPING; a_request_methods: detachable WSF_REQUEST_METHODS): WSF_ROUTER_MAPPING_DOCUMENTATION -- Documentation associated with Current handler, in the context of the mapping `m' and methods `a_request_methods'. --| `m' and `a_request_methods' are useful to produce specific documentation when the handler is used for multiple mapping. + require + m_attached: m /= Void + a_request_methods_attached: a_request_methods /= Void deferred + ensure + mapping_documentation_attached: Result /= Void end end diff --git a/library/server/wsf/router/wsf_handler.e b/library/server/wsf/router/wsf_handler.e index 1470a08d..3d15e03f 100644 --- a/library/server/wsf/router/wsf_handler.e +++ b/library/server/wsf/router/wsf_handler.e @@ -11,6 +11,8 @@ feature -- Status report is_valid_context (req: WSF_REQUEST): BOOLEAN -- Is `req' valid context for current handler? + require + req_attached: req /= Void do Result := True end @@ -19,6 +21,8 @@ feature {WSF_ROUTER} -- Mapping on_mapped (a_mapping: WSF_ROUTER_MAPPING; a_rqst_methods: detachable WSF_REQUEST_METHODS) -- Callback called when a router map a route to Current handler + require + a_mapping_attached: a_mapping /= Void do end