Invariants for methods

[Jens Mueller]

Andrei Alexandrescu wrote:
> On 11/18/10 1:57 PM, Jens Mueller wrote:
> >bearophile wrote:
> >>Jens Mueller:
> >>
> >>>I don't like the "old" approach.
> >>
> >>Why?
> >>(It's the canonical way to solve the problem you have had. It is present in Eiffel and C# and probably something similar is present in the DbC for Java. But surely other solutions are possible.)
> >
> >Somehow it doesn't feel right to me. It should just copy what is needed.
> >Let's say I have some very big object. Now old is a copy before the
> >execution of my member function. But I only check some little detail but
> >I end of with having this big copy. I think the programmer knows what
> >she's doing and she should have control about it. This copying behind the
> >scenes seems surprising to me. Maybe I do not fully understand the
> >approach.
> 
> The technique could be achieved by making "old" a keyword and
> copying only the fields accessed via "old". This approach was on the
> table. It has enough vagaries for me to dislike it.
> 
> One approach that I very much prefer is that the "out" contract sees
> the scope of the "in" contract. That way, the user can define state
> in the "in" contract and then check it in the "out" contract. The
> approach is more general and easier to understand than the one based
> on the "old" object.

I see. bearophile even has a bug for this problem
(http://d.puremagic.com/issues/show_bug.cgi?id=5027). Somehow that does
not surprise me. But I like it.

Even though there seems to be some disagreement on a proper solution
(right?) I think for the moment it's enough to have this bug report. In
particular I'm not sure whether bearophile agrees with having the out
contract seeing the in contract's scope. But if that's a valid solution
maybe he can add it to his bug report.

Jens