backup/EWF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Sixth round of contracts for non-Void-safe users

Browse Source
This commit is contained in:
Colin Adams
2013-03-15 14:50:59 +00:00
parent acc0f4ae94
commit 2d439a2414
3 changed files with 27 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e
View File

@@ -26,14 +26,27 @@ create
feature {NONE} -- Initialization feature {NONE} -- Initialization
make (a_router: WSF_ROUTER) make (a_router: WSF_ROUTER)
-- Initialize `router'.
require
a_router_attached: a_router /= Void
do do
router := a_router router := a_router
ensure
router_aliased: router = a_router
not_hidden: not is_hidden
end end
make_hidden (a_router: WSF_ROUTER) make_hidden (a_router: WSF_ROUTER)
-- Initialize `router'.
-- Do not display documentation for `a_router'.
require
a_router_attached: a_router /= Void
do do
make (a_router) make (a_router)
is_hidden := True is_hidden := True
ensure
router_aliased: router = a_router
hidden: is_hidden
end end
router: WSF_ROUTER router: WSF_ROUTER
@@ -46,6 +59,7 @@ feature {NONE} -- Initialization
feature -- Documentation feature -- Documentation
mapping_documentation (m: WSF_ROUTER_MAPPING; a_request_methods: detachable WSF_REQUEST_METHODS): WSF_ROUTER_MAPPING_DOCUMENTATION mapping_documentation (m: WSF_ROUTER_MAPPING; a_request_methods: detachable WSF_REQUEST_METHODS): WSF_ROUTER_MAPPING_DOCUMENTATION
-- <Precursor>
do do
create Result.make (m) create Result.make (m)
Result.set_is_hidden (is_hidden) Result.set_is_hidden (is_hidden)
@@ -76,4 +90,8 @@ feature -- Execution
res.send (m) res.send (m)
end end
invariant
router_attached: router /= Void
end end

5
library/server/wsf/router/documentation/wsf_self_documented_handler.e
View File

@@ -12,7 +12,12 @@ feature -- Documentation
mapping_documentation (m: WSF_ROUTER_MAPPING; a_request_methods: detachable WSF_REQUEST_METHODS): WSF_ROUTER_MAPPING_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'. -- 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. --| `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 deferred
ensure
mapping_documentation_attached: Result /= Void
end end
end end

4
library/server/wsf/router/wsf_handler.e
View File

@@ -11,6 +11,8 @@ feature -- Status report
is_valid_context (req: WSF_REQUEST): BOOLEAN is_valid_context (req: WSF_REQUEST): BOOLEAN
-- Is `req' valid context for current handler? -- Is `req' valid context for current handler?
require
req_attached: req /= Void
do do
Result := True Result := True
end end
@@ -19,6 +21,8 @@ feature {WSF_ROUTER} -- Mapping
on_mapped (a_mapping: WSF_ROUTER_MAPPING; a_rqst_methods: detachable WSF_REQUEST_METHODS) 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 -- Callback called when a router map a route to Current handler
require
a_mapping_attached: a_mapping /= Void
do do
end end