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

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.

On 2011-04-11 16:32:36 +0200, Kai Meyer said:

> 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.

Yeah, that's what I've got right now. Just seems odd to need to use attributes for this sort of thing. Also, it's rather brittle -- for example, if the function (directly or indirectly) calls itself. Then two (or more) pairs of in/out blocks will manipulate the same attribute... Seems like a variable that would be local to one specific in/out instantiation (or stack frame) would be preferable.

I guess I could just use a local variable (guarded by version()) and then have an assert() near the end of the function. Probably a better solution...

-- 
Magnus Lie Hetland
http://hetland.org

Magnus Lie Hetland:

> Yeah, that's what I've got right now. Just seems odd to need to use attributes for this sort of thing. Also, it's rather brittle -- for example, if the function (directly or indirectly) calls itself. Then two (or more) pairs of in/out blocks will manipulate the same attribute... Seems like a variable that would be local to one specific in/out instantiation (or stack frame) would be preferable.
> 
> I guess I could just use a local variable (guarded by version()) and then have an assert() near the end of the function. Probably a better solution...

Your need is perfectly natural it's named "old" values or prestate in contract programming, and currently it's probably the biggest hole in the D contract programming. It was discussed three or four times, like:

http://www.digitalmars.com/d/archives/digitalmars/D/why_no_old_operator_in_function_postconditions_as_in_Eiffel_54654.html

http://www.digitalmars.com/d/archives/digitalmars/D/Communicating_between_in_and_out_contracts_98252.html

I don't know if Walter is willing someday to fill this hole of the D DbC.

In my opinion is good to bugger now and then the main D newsgroup about this, to help Walter&Andrei understand that there are some programmers that care for this feature of DbC.

Bye,
bearophile

On 04/11/2011 04:36 PM, Magnus Lie Hetland wrote:
> I guess I could just use a local variable (guarded by version()) and then have
> an assert() near the end of the function. Probably a better solution...

If you mean coding your checking "by habd" inside the func's "normal" body, this seems to me the right solution. In any case, much simpler and less contorsed than declaring an additional attribute just for that. I would add a comment note telling why it's coded that way (asp. if you use contracts elsewhere).
Contracts, like any software tool, do not correctly match all possibly needs.

Denis
-- 
_________________
vita es estrany
spir.wikidot.com

spir:

> Contracts, like any software tool, do not correctly match all possibly needs.

This is true in general, but this isn't true in this case: here they don't match a basic need because D DbC misses a significant feature (prestate). If you take a look at other implementations of DbC in Eiffel and C# the prestate is present.

Bye,
bearophile

On 04/11/2011 09:18 PM, bearophile wrote:
> spir:
>
>> Contracts, like any software tool, do not correctly match all possibly needs.
>
> This is true in general, but this isn't true in this case: here they don't match a basic need because D DbC misses a significant feature (prestate). If you take a look at other implementations of DbC in Eiffel and C# the prestate is present.

Right, did not know that. Thnaks for this useful info.

Denis
-- 
_________________
vita es estrany
spir.wikidot.com

On 2011-04-11 18:42:18 +0200, bearophile said:

> Your need is perfectly natural it's named "old" values or prestate in contract programming, and currently it's probably the biggest hole in the D contract programming. It was discussed three or four times, like:
[snip]

Interesting.

> I don't know if Walter is willing someday to fill this hole of the D DbC.

It seems the prestate thing hasn't been done because it's a bit ambitious? I mean, the automatic part (which would be totally *kick-ass*, of course).

For me, I'd be happy if I could simply declare and initialize the variables myself somehow before the body is executed, and then check them in the out-block.

> In my opinion is good to bugger now and then the main D newsgroup about this, to help Walter&Andrei understand that there are some programmers that care for this feature of DbC.

Is there a feature request on this that I could add my vote to? If not, perhaps it's worth creating one?

If not, I guess I could just post a "bump" to the D group :-}

-- 
Magnus Lie Hetland
http://hetland.org

Magnus Lie Hetland:

> For me, I'd be happy if I could simply declare and initialize the variables myself somehow before the body is executed, and then check them in the out-block.

Indeed, as you may have seen in the linked threads, this was the main proposal in D. For me it's acceptable, if it works.


> Is there a feature request on this that I could add my vote to? If not, perhaps it's worth creating one?

I don't know of any feature request on this (I have opened bug 5027 about ghost fields, but now I am less interested in them), so search for it in Bugzilla. If you don't find it, then it's worth adding, with plenty of explanations of its purposes and ideas of ways to implement it.


> If not, I guess I could just post a "bump" to the D group :-}

I think lately Walter has lost a bit of enthusiasm regarding Design By Contract. A little bump once in a while is acceptable, to show that some people care for this sub-feature. If you want to (gently) bump then you may do after writing the bug report and showing the bug report number.

Bye,
bearophile