Eiffel "Gotchas"

07 April 1998

Gotcha #12 - onceness and invariants

This "gotcha" is rather subtle and complex. It's also vendor dependent - the behaviour described here occurs with ISE Eiffel.

Consider this class:

   class A
   feature
      foo: STRING is
         once
            result := "gotcha"
         end
   invariant
      foo_not_void: foo /= void
   end

The invariant seems safe - feature 'foo' will always return the string "gotcha", which is non-void, so the invariant can never fail.

But it does fail! Execution of the following system...

   class MAIN
   creation make
   feature
      make is
         local
            a: A
            s: STRING
         do
            !!a
            s := a.foo
         end
   end

...gives an invariant violation saying that 'foo' is void!

What's going on here?

ANSWER

Eiffel and NICE are registered trademarks of the Nonprofit International Consortium for Eiffel.

Eiffel "Gotchas"