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

The folks at Microsoft working on Spec# [1] have some interesting
thoughts in this vein, although I don't know how nicely they would
apply to either our contract or our class system.

sam th

[1]  http://research.microsoft.com/specsharp/#pubs

On 5/17/07, Robby Findler <robby at cs.uchicago.edu> wrote:
> 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
> >
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>


-- 
sam th
samth at ccs.neu.edu