[plt-scheme] contracts.ss: Class invariants?

From: Robby Findler (robby at cs.uchicago.edu)
Date: Thu May 17 09:24:08 EDT 2007

I have thought about them some, but I've always found them troubling.
The word "invariant" means that this property is always true, right?
And yet invariants certainly are NOT always true. Typically,
invariants are implemented by checking an invariant of an object when
any method is called and again when any method returns.

The intuition there is that the invariant should be true when
something outside the object interacts with it. But of course, even
that's not the case, due to callbacks and threads.

So, since I feel like I don't know how to do them properly, I've just
left invariants out.

Of course, if that particular behavior is exactly what you need, you
can express it by putting the invariant into the pre- and
post-condition of each method, "manually".

Robby

On 5/16/07, Grant Rettke <grettke at acm.org> wrote:
> Is anyone looking at class invariants for the future in contracts?
>
> It is not a deal breaker for me or anything, just wondering if that is
> an interesting feature or not.
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>


Posted on the users mailing list.