The invariant and code are contradictory for XM_NAMESPACE
invariant
uri_not_void: uri /= Void
But code handle the case it is Void
is_equal (other: like Current): BOOLEAN is
-- Are the two namespaces equal?
do
Result := (uri = other.uri) or else
(uri /= Void and then STRING_.same_string (uri,
other.uri))
ensure then
definition: Result = STRING_.same_string (uri, other.uri)
end
hash_code: INTEGER is
-- Hash code of URI.
do
if uri /= Void then
Result := uri.hash_code
end
end
out: STRING is
-- Out.
do
if uri = Void then
Result := ""
else
Result := uri
end
end
However, the creation procedure's implementation ensure `uri' is never Void.
Suggestion: keep invariant, and remove case where `uri' can be Void
------------------------------------------------------------------------------
This SF.net email is sponsored by:
SourcForge Community
SourceForge wants to tell your story.
http://p.sf.net/sfu/sf-spreadtheword_______________________________________________
gobo-eiffel-develop mailing list
[hidden email]
https://lists.sourceforge.net/lists/listinfo/gobo-eiffel-develop
