I'd like to write a contract for a method to ensure that a given
attribute does not decrease when calling the method. In order to do
that, I need to store the "before" value, and compare it to the after
value.
My first intuition was to declare a variable in the in-block, and then
access that in the out-block. No dice, it seems. I tried declaring one
in the body (with a version(unittest) qualifier). Still no dice. I
ended up using a separate *attribute* for this, which seems
particularly ugly to me.
Is it philosophically "wrong" to write stateful "before/after"
contracts like this? If not, can it be done in a less ugly manner? (Or
should I just learn to like this way of doing it?)
--
Magnus Lie Hetland
http://hetland.org
