Invariants for methods

[Andrei Alexandrescu]

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.


Andrei