Class features

[Reto Weber]

I have in the class ANY a class feature universe (which is only used for static verification and cannot be executed).

universe: MML_SET [ANY]
-- Set of all objects.
note
status: ghost
do
check is_executable: False then end
ensure
instance_free: class
end

Now I have a different class

class
THEORY [G -> ANY]
feature

do_something

require

    not {G}.universe.is_empty

do

      ...

end

But this does not compile anymore.

Non-object call on a non-class type Generic #1.

Error code: VUNO

The non-object call uses a target type Generic #1 that is not a class type.

What to do: Make sure the target type of the non-object call is an effective class type.

Class: THEORY [G -> ANY]
Feature:  do_something
Line: 99
      require
->      not {G}.universe.is_empty

For me this is a bug. Does anybody have a workaround how to invoke such features in a contract?

[Ulrich Windl]

What's the purpose of "then" in "check"?

29.04.2025 11:53:43 Reto Weber <reto.a...@gmail.com>:

> False then

[Reto Weber]

This is irrelevant for my problem. I think this way the line survives compilation when setting the flag "assertions.check" to False in the project settings.

[Ilgiz Mustafin]

Try to add "( )" parenthesis like this: ({G}).universe

среда, 30 апреля 2025 г. в 12:00:40 UTC, reto.a...@gmail.com: