"Before and after" in contracts?

[Magnus Lie Hetland]

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