[review] error in XM_NAMESPACE

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