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