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
|
