Re: [gobo-eiffel-develop] [review] error in XM_NAMESPACE

[Eric B. <er...@go...>]

Jocelyn wrote:
> 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

Done.

-- 
Eric Bezault
mailto:er...@go...
http://www.gobosoft.com