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

[Jocelyn <li...@dj...>]

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