Search code examples
invariantseiffel

Invariant sharing with Eiffel's keyword `like`

In Eiffel, it is possible to specify a type with an 'anchored declaration'.

I wonder if the relevant invariants in the class also apply to an anchored declaration:

class C

feature

    f: INTEGER
        do
            ... Do something ...
        end

    g: like f
        do
            ... Do some other thing ...
        end

invariant
    0 < f
    -- 0 < g  <-- Does this pop into existence?
end

I didn't see this written anywhere, and I think it's not the case. It would be convenient, sometimes, to avoid defining yet another type, but I think that would restrict the usefulness of anchored declarations in all other cases.

Solution

  • No, it is not possible to automagically create an invariant from an anchored declaration. In the line:

    g: like f

    the anchor type "like f" only replace the type of "g". It is very similar to copy and paste the type of "f" as the type of "g". In other word, in your example, what you write is almost the same as writing directly:

    g: INTEGER