Problem with contracts

[Charles]

I ran into this tonight while coding up a class library. Here is the distilled version of the problem:

class A

    pro x from var = 1
    
    def setX(x as int)
        _x = x

class B inherits A

    invariant
        .x > 0

    def foo
        pass

class P

    def main
        b = B()
        b.foo
        
        b.x = 0    # should fail B's invariant
        b.setX(0)  # should fail B's invariant

Any Eiffel users out there? Am I correct that B's additional invariant (.x > 0) should cause an exception when members inherited from A (.x and .setX) are used to violate it?

Currently the above code executes with no exceptions because the member's of A don't bother to check invariants (due to their not being any invariants for A). I think this is a bug. Comments welcome.

-Chuck

[jonathandavid]

I think this issue was already discussed...

viewtopic.php?f=4&t=237&hilit=invariant

[Charles]

Ah thanks. This was feeling familiar and now that thread brings it all back...

Ug!

So if we had an IL backend, we could side step C#'s requirement that the first statement of a constructor is a call to another constructor which would make one of my proposed treatments workable.

Anybody got some free time?

But also you proposed here that the end of a constructor call the non-polymorphic invariant, although this isn't completely bullet proof as explained in my next post.