Page 1 of 1

Problem with contracts

PostPosted: Tue Sep 15, 2009 2:58 am
by 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

Re: Problem with contracts

PostPosted: Wed Sep 16, 2009 6:17 am
by jonathandavid
I think this issue was already discussed...

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

Re: Problem with contracts

PostPosted: Fri Sep 18, 2009 7:24 am
by 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? :-D

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.