Communicating between in and out contracts

[Rainer Deyke]

Leandro Lucarella wrote:
> Rainer Deyke, el 17 de octubre a las 14:24 me escribiste:
>> There is no "the object".
> There is an object if you have this:
> 
> void f(SomeObjectWithLotsOfReferences obj) out {
>   assert(old(obj).some_check());
> }

If 'obj' is a reference type and the reference itself wasn't modified,
then 'old(obj)' is the same as 'obj'.  Objects are only copied if you
explicitly copy them.  'old(x)' means "the cached value of evaluating
'x' at the beginning of the routine".  No more, no less.


-- 
Rainer Deyke - rainerd at eldwood.com