www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.learn - "Before and after" in contracts?

reply Magnus Lie Hetland <magnus hetland.org> writes:
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
Apr 11 2011
next sibling parent reply Kai Meyer <kai unixlords.com> writes:
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.
Apr 11 2011
next sibling parent reply Magnus Lie Hetland <magnus hetland.org> writes:
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
Apr 11 2011
next sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
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
Apr 11 2011
parent reply Magnus Lie Hetland <magnus hetland.org> writes:
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:

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
Apr 13 2011
parent bearophile <bearophileHUGS lycos.com> writes:
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
Apr 13 2011
prev sibling parent bearophile <bearophileHUGS lycos.com> writes:
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
Apr 11 2011
prev sibling parent spir <denis.spir gmail.com> writes:
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
Apr 11 2011
prev sibling parent spir <denis.spir gmail.com> writes:
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
Apr 11 2011