Eiffel "Gotchas"

07 April 1998

Gotcha #12 - Answer and Explanation

Here's the question again:

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?

Let's start with the instruction "s := a.foo". ETL p133 states:

If r is a routine of a class C, a call is qualified if it is of the form "a.r(...)" with an explicit target, here a ... such a qualified call will cause the invariant to be evaluated (both before and after the call) ...

So, we have a qualified call, and the invariant of a will be evaluated before the call "a.foo". The invariant of a is the expression "foo /= void".

Let's look first at what happens on a compiler that does not fail the invariant (I observed this behaviour with Visual Eiffel 2.0g):

The expression "foo /= void" causes the body of foo to be executed. This returns the string "gotcha", which is non-void, so the invariant is true, and execution proceeds to "a.foo". Because foo is a once-function that has already been executed, the result from the previous call is returned. This is again the string "gotcha", and no assertion failure has occurred.

Before we can understand why the ISE compiler fails the invariant, we need to look "under the hood" at the implementation of once-functions. Conceptually, there is a boolean flag that is set when a once-function is executed, and a storage area to record the result. When the once-function is called, the flag is examined. If the flag is set, the result is obtained from the storage area. Otherwise, the result is obtained by executing the body of the once-function. We can express this in pseudocode:

   if not execution_started then
      execution_started := true
      (perform the body of the function, setting recorded_value
      after every assignment to 'result')
   end
   result := recorded_value

Notice that we call our boolean flag execution_started, and set it at the start of the execution of the body of the once-function. This ensures that in the event of a recursive call, our once-function will work as per ETL p353. That is, the recursive call will return the value computed by the enclosing call up to the point of the recursive call. This keeps things simple, because we only need one storage area (recorded_value) rather than a stack of them.

When we add invariant-testing to this pseudocode, we have two choices. We can test the invariant either outside or inside the part of the code guarded by the test against execution_started. If we write it as follows, we get the behaviour observed in Visual Eiffel 2.0g:

   if remote call then
      check invariant
      -- the invariant includes a non-remote call to 'foo', which sets
      -- 'execution_started' to true and sets 'recorded_value' to "gotcha"
   end
   if not execution_started then
      execution_started := true
      (perform the body of the function, setting recorded_value
      after every assignment to 'result')
   end
   result := recorded_value

I'm guessing that the ISE compiler uses the following scheme or something similar:

   if not execution_started then
      execution_started := true
      if remote call then
         check invariant -- causes recursive call to 'foo'
      end
      (perform the body of the function, setting recorded_value
      after every assignment to 'result')
   end
   result := recorded_value

In this case, when the invariant is checked the execution_started flag will already be true, and the recursive call to foo will return the value so far stored in recorded_value, i.e. the default initialization of result which is void. Therefore, the invariant will fail.

As far as I can tell, ETL does not specifically address whether assertions must be checked for every call to a once-function, or just for the first call:

... a qualified call will cause the invariant to be evaluted (both before and after the call) ... [p133-4]

 

... if 'df' is a [once-]function, its sole effect is to return the value of 'result' as computed by the first call to 'df'. If, however, this is the first call to 'df' in the current system execution, the effect is exactly the same as for a non-once routine ... [p353]

My interpretation is that assertions must be checked for every call, based on the assumption that p133 specifies additional behaviour rather than a modification of the behaviour described on p353.

However, it seems that ISE takes a different interpretation (and after all, Bertrand Meyer did write the book so he should know what is intended).

Thanks to Eric Bezault for suggesting this Gotcha.

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

Eiffel "Gotchas"