Output contract's arguements

Joseph Rushton Wakeling joseph.wakeling at webdrake.net
Thu Sep 19 05:44:55 PDT 2013


On 19/09/13 14:19, Peter Alexander wrote:
> You mean a separate copy from v?
>
> But surely then the copy would *always* be the same in the in-contract as it is
> in the out-contract? What's the point?

It makes sense to be able to access v.old (or v.onEntry or whatever you want to 
call it) in the out contract, as then you could do some checks on the final 
value of v that are dependent on its entry value.

e.g. you might have a function where this kind of rule holds:

     assert((v && !v.old) || (!v && v.old));

i.e. if it's 0 on entry, it must be non-zero on exit, and vice versa.

But it doesn't make sense to me that v in the out contract would refer to the 
value of v on entry to the function.


More information about the Digitalmars-d mailing list