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


[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
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 reply 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
parent reply 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

is present.

Bye,
bearophile
Apr 11 2011
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

is present.


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

Denis
-- 
_________________
vita es estrany
spir.wikidot.com
Apr 11 2011