"Before and after" in contracts?

[Kai Meyer]

On 04/11/2011 06:05 AM, Magnus Lie Hetland wrote:
> 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?)
>

I don't know if I can speak to the philosophical points here, but you 
can put your attribute declarations in a version block, and as long as 
the usage of that attribute is only used when that version is used, you 
should be fine.