www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - why no "old" operator in function postconditions, as in Eiffel?

reply Russ Williams <digitalmars.D.learn russcon.removethispart.andthis.org> writes:
I have started exploring D; a big attraction for me is the Design By Contract
support.  So I am quite surprised and disappointed that there is no "old"
operator as in Eiffel, to permit a function postcondition to mention values
from function entry.  E.g. a container class might have something like:

void insertFoo(Foo f)
out
{
    assert(fooCount == old(fooCount) + 1);
}

or a City class in a game might have something like:
void buildStuff(int n)
out
{
    assert(resourceCount == old(resourceCount) - n);
    assert(stuffCount == old(stuffCount) + n);
}

(to give a couple of simplified examples)

I regard this is a crucial part of DbC (similar to the language and compiler
automatically handling inheritance of pre/postconditions, for instance);
without this ability, function postconditions are quite crippled and much less
expressive.  Any function that changes the state of "this" and depends on the
starting state of "this" wants to use "old" in the postcondition to explain the
behavior.

Being a newbie, I already asked in the digitalmars.D.learn ... no one there
knew of a way to do this directly, only with various additional explicit
boilerplate coding by the programmer.  That's not good... It seems like D's DbC
support is pointlessly crippled by this missing "old" functionality, which
would not be hard to add.  (The compiler just generates code to make a local
variables to evaluate and save the value of expressions which are mentioned in
"old" expressions in the function's postcondition.  Exactly the sort of
repetitive tedium that the programmer shouldn't have to do.)

Are there plans to add such support to D?  Searching the archives for "old" and
"Eiffel" and find virtually no mention of this, which amazes me.  I found "old"
to be extremely useful when I coded in Eiffel.  Not having it in a language
that bills itself as supporting DbC seems like languages which only have
"assert" and claim to be supporting DbC.
Jun 18 2007
next sibling parent reply davidl <davidl 126.com> writes:
That feature doesn't worth a keyword at all, and old(blah) pollutes the
naming space. You have several choices already:

The following shows how your old keyword should work(NOTICE: the code  
would probably be not compatible with D2.0):

int func(int n)
out(result)
{
	static int[int] funcmap;	// create a func mapping here for further old  
keyword test
					// while this kind of sanity test would bloat the AA funcmap greatly
					// But I don't see any other solution without increasing runtime to  
solve this
					// problem in *any* other language
	funcmap[n]=result;
	if ((n-1) in funcmap)		// test if that has been calculated
		assert(funcmap[n]==funcmap[n-1]+1);
}
body
{
	if (n<1) return 0;
	return func(n-1)+1;
}
void main()
{
	func(3);
}




 I have started exploring D; a big attraction for me is the Design By  
 Contract support.  So I am quite surprised and disappointed that there  
 is no "old" operator as in Eiffel, to permit a function postcondition to  
 mention values from function entry.  E.g. a container class might have  
 something like:

 void insertFoo(Foo f)
 out
 {
     assert(fooCount == old(fooCount) + 1);
 }

 or a City class in a game might have something like:
 void buildStuff(int n)
 out
 {
     assert(resourceCount == old(resourceCount) - n);
     assert(stuffCount == old(stuffCount) + n);
 }

 (to give a couple of simplified examples)

 I regard this is a crucial part of DbC (similar to the language and  
 compiler automatically handling inheritance of pre/postconditions, for  
 instance); without this ability, function postconditions are quite  
 crippled and much less expressive.  Any function that changes the state  
 of "this" and depends on the starting state of "this" wants to use "old"  
 in the postcondition to explain the behavior.

 Being a newbie, I already asked in the digitalmars.D.learn ... no one  
 there knew of a way to do this directly, only with various additional  
 explicit boilerplate coding by the programmer.  That's not good... It  
 seems like D's DbC support is pointlessly crippled by this missing "old"  
 functionality, which would not be hard to add.  (The compiler just  
 generates code to make a local variables to evaluate and save the value  
 of expressions which are mentioned in "old" expressions in the  
 function's postcondition.  Exactly the sort of repetitive tedium that  
 the programmer shouldn't have to do.)

 Are there plans to add such support to D?  Searching the archives for  
 "old" and "Eiffel" and find virtually no mention of this, which amazes  
 me.  I found "old" to be extremely useful when I coded in Eiffel.  Not  
 having it in a language that bills itself as supporting DbC seems like  
 languages which only have "assert" and claim to be supporting DbC.




-- 
使用 Opera 革命性的电子邮件客户程序: http://www.opera.com/mail/
Jun 18 2007
parent reply Jari-Matti =?ISO-8859-1?Q?M=E4kel=E4?= <jmjmak utu.fi.invalid> writes:
davidl wrote:


 That feature doesn't worth a keyword at all, and old(blah) pollutes the
 naming space. You have several choices already:
 
 The following shows how your old keyword should work(NOTICE: the code
 would probably be not compatible with D2.0):
 
 int func(int n)
 out(result)
 {
 static int[int] funcmap;      // create a func mapping here for further old
 keyword test
 // while this kind of sanity test would bloat the AA funcmap greatly
 // But I don't see any other solution without increasing runtime to
 solve this
 // problem in *any* other language
 funcmap[n]=result;
 if ((n-1) in funcmap)         // test if that has been calculated
 assert(funcmap[n]==funcmap[n-1]+1);
 }
 body
 {
 if (n<1) return 0;
 return func(n-1)+1;
 }
 void main()
 {
 func(3);
 }
 


What is this supposed to solve? DbC is supposed to save the high level
representation of contracts. Also inheritance as implemented currently
breaks your example and your function is stateless, so there's absolutely
no need for 'old' in that.


 Being a newbie, I already asked in the digitalmars.D.learn ... no one
 there knew of a way to do this directly, only with various additional
 explicit boilerplate coding by the programmer.




You can always extend the language with metaprogramming. ;)


 Are there plans to add such support to D?  Searching the archives for
 "old" and "Eiffel" and find virtually no mention of this, which amazes
 me.  I found "old" to be extremely useful when I coded in Eiffel.  Not
 having it in a language that bills itself as supporting DbC seems like
 languages which only have "assert" and claim to be supporting DbC.




I hope so. DbC in most languages is a bad joke. They teach you to use  pre
and  post in javadoc comments in uni these days, but seriously nobody is
going to use it (correctly) if the compiler cannot enforce anything. That's
the whole point.
Jun 20 2007
parent davidl <davidl 126.com> writes:
wah, why following my post? looks like a CON-post while it's not :)

Yes, you pointed things out more clearly, "old" keyword as mentioned
only works for the stateless function. And DbC is actually not tho-
roughly or widely viewed carefully enough.


 davidl wrote:


 That feature doesn't worth a keyword at all, and old(blah) pollutes the
 naming space. You have several choices already:

 The following shows how your old keyword should work(NOTICE: the code
 would probably be not compatible with D2.0):

 int func(int n)
 out(result)
 {
 static int[int] funcmap;      // create a func mapping here for further  
 old
 keyword test
 // while this kind of sanity test would bloat the AA funcmap greatly
 // But I don't see any other solution without increasing runtime to
 solve this
 // problem in *any* other language
 funcmap[n]=result;
 if ((n-1) in funcmap)         // test if that has been calculated
 assert(funcmap[n]==funcmap[n-1]+1);
 }
 body
 {
 if (n<1) return 0;
 return func(n-1)+1;
 }
 void main()
 {
 func(3);
 }


 What is this supposed to solve? DbC is supposed to save the high level
 representation of contracts. Also inheritance as implemented currently
 breaks your example and your function is stateless, so there's absolutely
 no need for 'old' in that.


 Being a newbie, I already asked in the digitalmars.D.learn ... no one
 there knew of a way to do this directly, only with various additional
 explicit boilerplate coding by the programmer.




 You can always extend the language with metaprogramming. ;)


 Are there plans to add such support to D?  Searching the archives for
 "old" and "Eiffel" and find virtually no mention of this, which amazes
 me.  I found "old" to be extremely useful when I coded in Eiffel.  Not
 having it in a language that bills itself as supporting DbC seems like
 languages which only have "assert" and claim to be supporting DbC.




 I hope so. DbC in most languages is a bad joke. They teach you to use  
  pre
 and  post in javadoc comments in uni these days, but seriously nobody is
 going to use it (correctly) if the compiler cannot enforce anything.  
 That's
 the whole point.




-- 
使用 Opera 革命性的电子邮件客户程序: http://www.opera.com/mail/
Jun 20 2007
prev sibling parent reply Bruno Medeiros <brunodomedeiros+spam com.gmail> writes:
Russ Williams wrote:

 I have started exploring D; a big attraction for me is the Design By Contract
support.  So I am quite surprised and disappointed that there is no "old"
operator as in Eiffel, to permit a function postcondition to mention values
from function entry.  E.g. a container class might have something like:
 
 void insertFoo(Foo f)
 out
 {
     assert(fooCount == old(fooCount) + 1);
 }
 
 or a City class in a game might have something like:
 void buildStuff(int n)
 out
 {
     assert(resourceCount == old(resourceCount) - n);
     assert(stuffCount == old(stuffCount) + n);
 }
 
 (to give a couple of simplified examples)
 
 I regard this is a crucial part of DbC (similar to the language and compiler
automatically handling inheritance of pre/postconditions, for instance);
without this ability, function postconditions are quite crippled and much less
expressive.  Any function that changes the state of "this" and depends on the
starting state of "this" wants to use "old" in the postcondition to explain the
behavior.
 
 Being a newbie, I already asked in the digitalmars.D.learn ... no one there
knew of a way to do this directly, only with various additional explicit
boilerplate coding by the programmer.  That's not good... It seems like D's DbC
support is pointlessly crippled by this missing "old" functionality, which
would not be hard to add.  (The compiler just generates code to make a local
variables to evaluate and save the value of expressions which are mentioned in
"old" expressions in the function's postcondition.  Exactly the sort of
repetitive tedium that the programmer shouldn't have to do.)
 
 Are there plans to add such support to D?  Searching the archives for "old"
and "Eiffel" and find virtually no mention of this, which amazes me.  I found
"old" to be extremely useful when I coded in Eiffel.  Not having it in a
language that bills itself as supporting DbC seems like languages which only
have "assert" and claim to be supporting DbC.


For D to properly support 'old', D would need to clone any input used as 
old, and that sounds as it might have some issues (not sure about that 
though). Still, perhaps better would be the alternative presented in the 
.learn thread where the 'out' scope would be able to access the 'in' scope.

-- 
Bruno Medeiros - MSc in CS/E student
http://www.prowiki.org/wiki4d/wiki.cgi?BrunoMedeiros#D
Jun 21 2007
parent reply Frits van Bommel <fvbommel REMwOVExCAPSs.nl> writes:
Bruno Medeiros wrote:

 For D to properly support 'old', D would need to clone any input used as 
 old, and that sounds as it might have some issues (not sure about that 
 though). Still, perhaps better would be the alternative presented in the 
 .learn thread where the 'out' scope would be able to access the 'in' scope.


I don't think cloning is necessary. It would just need to evaluate the 
old-expression before the body is entered (i.e. at the end of the "in" 
clause) and save the result in an "invisible variable" that's accessed 
where the old-expression appears.
Of course, it's then the programmer's responsibility to make sure that 
the result is still valid after the body has executed; if it for 
instance slices an array that's modified in the function, manual dups 
will be required.
Jun 22 2007
next sibling parent reply Daniel Keep <daniel.keep.lists gmail.com> writes:
Frits van Bommel wrote:

 Bruno Medeiros wrote:

 For D to properly support 'old', D would need to clone any input used
 as old, and that sounds as it might have some issues (not sure about
 that though). Still, perhaps better would be the alternative presented
 in the .learn thread where the 'out' scope would be able to access the
 'in' scope.


 
 I don't think cloning is necessary. It would just need to evaluate the
 old-expression before the body is entered (i.e. at the end of the "in"
 clause) and save the result in an "invisible variable" that's accessed
 where the old-expression appears.
 Of course, it's then the programmer's responsibility to make sure that
 the result is still valid after the body has executed; if it for
 instance slices an array that's modified in the function, manual dups
 will be required.


Maybe, and I realise this might be a really ugly, hackish way to do it,
we should make "old" a special storage class.  A variable defined as
"old" in an out contract is evaluated before the function body.  This
solves this "how do we clone these things?", since the programmer can
write any initialiser that makes sense, and it clearly demarcates these
special cases.

Of course, the problem then is that the code will be *really*
counter-intuitive.

void foo()
out
{
    // gets evaluated *before* body... wtf?
    old bar = this.bar.theDupFunction();
}
body
{
    // ...
}

	-- Daniel
Jun 22 2007
parent Jari-Matti =?ISO-8859-1?Q?M=E4kel=E4?= <jmjmak utu.fi.invalid> writes:
Daniel Keep wrote:

 Frits van Bommel wrote:

 Bruno Medeiros wrote:

 For D to properly support 'old', D would need to clone any input used
 as old, and that sounds as it might have some issues (not sure about
 that though). Still, perhaps better would be the alternative presented
 in the .learn thread where the 'out' scope would be able to access the
 'in' scope.


 
 I don't think cloning is necessary. It would just need to evaluate the
 old-expression before the body is entered (i.e. at the end of the "in"
 clause) and save the result in an "invisible variable" that's accessed
 where the old-expression appears.
 Of course, it's then the programmer's responsibility to make sure that
 the result is still valid after the body has executed; if it for
 instance slices an array that's modified in the function, manual dups
 will be required.


 
 Maybe, and I realise this might be a really ugly, hackish way to do it,
 we should make "old" a special storage class.  A variable defined as
 "old" in an out contract is evaluated before the function body.  This
 solves this "how do we clone these things?", since the programmer can
 write any initialiser that makes sense, and it clearly demarcates these
 special cases.


I have no experience with the 'old' concept in free functions, but I think a
class only needs to take care of its own members. If every class takes care
of their members, then all states are covered (at least according to some
OO principles). So I have initialized the old object implicitly before body
{} is executed and then accessed it in the out {} section. I have also
hidden the reference so it wont pollute the namespace. So far this has
worked fine (albeit the loss of syntax highlighting with string mixins is
not so nice - a compile time D parser would help a lot :) )
Jun 22 2007
prev sibling parent reply Bruno Medeiros <brunodomedeiros+spam com.gmail> writes:
Frits van Bommel wrote:

 Bruno Medeiros wrote:

 For D to properly support 'old', D would need to clone any input used 
 as old, and that sounds as it might have some issues (not sure about 
 that though). Still, perhaps better would be the alternative presented 
 in the .learn thread where the 'out' scope would be able to access the 
 'in' scope.


 
 I don't think cloning is necessary. It would just need to evaluate the 
 old-expression before the body is entered (i.e. at the end of the "in" 
 clause) and save the result in an "invisible variable" that's accessed 
 where the old-expression appears.
 Of course, it's then the programmer's responsibility to make sure that 
 the result is still valid after the body has executed; if it for 
 instance slices an array that's modified in the function, manual dups 
 will be required.


Well, yeah, if you only want old to work automatically for primitive 
types, then D itself wouldn't need to know how to clone. But if there 
will still be cases which need manual dups, then maybe its not worth it, 
versus the joined in-out scope alternative (where you have to manually 
dup any old you wish to check).

-- 
Bruno Medeiros - MSc in CS/E student
http://www.prowiki.org/wiki4d/wiki.cgi?BrunoMedeiros#D
Jun 23 2007
parent "David B. Held" <dheld codelogicconsulting.com> writes:
Bruno Medeiros wrote:

 [...]
 Well, yeah, if you only want old to work automatically for primitive 
 types, then D itself wouldn't need to know how to clone. But if there 
 will still be cases which need manual dups, then maybe its not worth it, 
 versus the joined in-out scope alternative (where you have to manually 
 dup any old you wish to check).


Not only that, but the type under consideration would have to *be* 
clonable.  D doesn't have first-class copy c'tors yet, but the ability 
to hide them would mean that some types would be non-copyable.  Of 
course, one could just say at that point that you either get a bitwise 
copy or you can't use the old operator on those variables.  But the 
"old" operator seems fairly non-trivial in any case.

Dave
Jun 28 2007