Eiffel "Gotcha" #12 - onceness and invariants 
Author Message
 Eiffel "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.

Thanks to Eric Bezault for submitting this one - he reports that two
of his colleagues were caught by it recently.

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?

Regards,
Roger
--
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.*-*-*.com/ | +44-1772-687525



Fri, 12 Nov 1999 03:00:00 GMT  
 Eiffel "Gotcha" #12 - onceness and invariants

Roger Browne:

Quote:
>             !!a
>             s := a.foo

Would the invariant be triggered between these two lines, because the
invariant is first checked before the first "real" call to foo, and the
"call" to foo in the invariant is implemented by the compiler in a way
that ignores the onceness?

(One could see a possible side-effect if it were implemented the other way,
that is the once variable would be initialised by the invariant, and so
initialised elsewhere or not at all in optimised programs).

Another compiler dependent trick with invariants is like:

class A creation make feature

  bool : BOOLEAN

  make is
    local b : B do
      !!b.make(Current)
      bool := true
    end

  nothing is do end

invariant
  bool = true

end

class B creation make feature

  make(a : A) is do a.nothing end

end

!!a.make -- invariant violation with some compilers



Fri, 12 Nov 1999 03:00:00 GMT  
 Eiffel "Gotcha" #12 - onceness and invariants

I don't think there is anything compiler-dependent
in the examples. The specification of assertion monitoring
in "Eiffel: The Language" (section 9.17, pages 132-134)
seems to me quite clear as to what must happen in
these cases.

        (Trifling aside: there is no need to define `nothing'
        since class GENERAL already includes `do_nothing'.)

--
Bertrand Meyer, President, ISE Inc., Santa Barbara (California)

Web page: http://www.eiffel.com
        (including instructions to download Eiffel 4 for Windows)



Fri, 12 Nov 1999 03:00:00 GMT  
 Eiffel "Gotcha" #12 - onceness and invariants

Quote:
> 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
in 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 like this,
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.

I find it quite hard to get my head around this stuff, and I've probably
missed some subtle details from this explanation, so if anything doesn't make
sense please ask and I'll try to clarify it.

Regards,
Roger
--
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.eiffel.demon.co.uk/ | +44-1772-687525



Sat, 13 Nov 1999 03:00:00 GMT  
 Eiffel "Gotcha" #12 - onceness and invariants

Quote:

> I don't think there is anything compiler-dependent
> in the examples.

The examples are "compiler-dependent" in the sense that different results are
obtained from the same source code, according to which compiler is being used.

Quote:
> The specification of assertion monitoring
> in "Eiffel: The Language" (section 9.17, pages 132-134)
> seems to me quite clear as to what must happen in
> these cases.

I am happy that ETL makes it clear that the invariant should fail in
Franck's example, because in this line...

      !!b.make(Current)

..we are passing an incompletely-initialized reference to 'current'.
As 'b' performs a remote call with target 'current', the invariant
must be checked and it must fail.

However, ETL p132-134 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 the former, 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).
Nevertheless, I'm sure a clarification from BM or NICE would be appreciated.

Regards,
Roger

PS: It might be a while before I can post any more "gotchas", as I have a busy
time coming up. If anyone missed any, they are available at
http://www.totalweb.co.uk/gustave/gotcha/
--
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.eiffel.demon.co.uk/ | +44-1772-687525



Sat, 13 Nov 1999 03:00:00 GMT  
 
 [ 7 post ] 

 Relevant Pages 

1. Eiffel "Gotcha" #10 - discounts

2. Eiffel "Gotcha" #10 - cleaning up

3. Eiffel "Gotcha" #9 - postconditions

4. Eiffel "Gotcha" #7 - redundant parentheses

5. TOOLS EUROPE 97: 2nd CFP (12-15 May "1007", Paris)

6. parse.y (version "2000-12-18")

7. SICP and "Loop Invariants"

8. TIP #12: The "Batteries Included" Distribution

9. TIP #12: The "Batteries Included" Distribution

10. TOOLS EUROPE 97: 2nd CFP (12-15 May "1007", Paris)

11. string.join(["Tk 4.2p2", "Python 1.4", "Win32", "free"], "for")

12. BEGIN{want[]={"s1o", "s2o", "s2q", "s3q"}

 

 
Powered by phpBB® Forum Software