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.
