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.

Reply via email to