Re: Before and after in contracts?

2011-04-13 Thread Magnus Lie Hetland

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



Re: Before and after in contracts?

2011-04-13 Thread bearophile
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


Before and after in contracts?

2011-04-11 Thread Magnus Lie Hetland
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



Re: Before and after in contracts?

2011-04-11 Thread 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.


Re: Before and after in contracts?

2011-04-11 Thread Magnus Lie Hetland

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



Re: Before and after in contracts?

2011-04-11 Thread bearophile
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 WalterAndrei understand that there are some programmers that care for 
this feature of DbC.

Bye,
bearophile


Re: Before and after in contracts?

2011-04-11 Thread spir

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



Re: Before and after in contracts?

2011-04-11 Thread bearophile
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


Re: Before and after in contracts?

2011-04-11 Thread spir

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