www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.learn - D's design by contract is missing "old"?

reply Russ <digitalmars.D.learn russcon.removethispart.andthistoo.org> writes:
As far as I can tell, there is no "old" (as in Eiffel) for the function
postconditions, which makes them a lot less useful.  "Old" is an essential part
of DBC.  The postcondition contract often wants to talk about how the resulting
object is different from the original state of the object.  
E.g. search for "old" on this page:
http://archive.eiffel.com/doc/manuals/technology/contract/

Here's a very simple example of what I want to do in D:

void twiddleFoo(int direction, int amount)
in
{
    assert(direction == UP || direction == DOWN);
}
out
{
    assert (direction == UP ? foo == old foo + amount : foo == old foo -
amount);
}

Is there away to achieve the effect of "old", i.e. for the "out" clause to
explicitly state that the value of "foo" has gone up or down by "amount"
according to the value of "direction"?  Am I not noticing something in D?
Jun 17 2007
next sibling parent janderson <askme me.com> writes:
Russ wrote:
 As far as I can tell, there is no "old" (as in Eiffel) for the function
postconditions, which makes them a lot less useful.  "Old" is an essential part
of DBC.  The postcondition contract often wants to talk about how the resulting
object is different from the original state of the object.  
 E.g. search for "old" on this page:
 http://archive.eiffel.com/doc/manuals/technology/contract/
 
 Here's a very simple example of what I want to do in D:
 
 void twiddleFoo(int direction, int amount)
 in
 {
     assert(direction == UP || direction == DOWN);
 }
 out
 {
     assert (direction == UP ? foo == old foo + amount : foo == old foo -
amount);
 }
 
 Is there away to achieve the effect of "old", i.e. for the "out" clause to
explicitly state that the value of "foo" has gone up or down by "amount"
according to the value of "direction"?  Am I not noticing something in D?

This looks like a neat idea. I imagine the D syntax may look more like: assert (direction == UP ? foo == old(foo) + amount : foo == old(foo) - zmount);
Jun 17 2007
prev sibling next sibling parent reply Daniel Keep <daniel.keep.lists gmail.com> writes:
Russ wrote:
 As far as I can tell, there is no "old" (as in Eiffel) for the function
postconditions, which makes them a lot less useful.  "Old" is an essential part
of DBC.  The postcondition contract often wants to talk about how the resulting
object is different from the original state of the object.  
 E.g. search for "old" on this page:
 http://archive.eiffel.com/doc/manuals/technology/contract/
 
 Here's a very simple example of what I want to do in D:
 
 void twiddleFoo(int direction, int amount)
 in
 {
     assert(direction == UP || direction == DOWN);
 }
 out
 {
     assert (direction == UP ? foo == old foo + amount : foo == old foo -
amount);
 }
 
 Is there away to achieve the effect of "old", i.e. for the "out" clause to
explicitly state that the value of "foo" has gone up or down by "amount"
according to the value of "direction"?  Am I not noticing something in D?

I found myself wanting something like this recently when I was writing a state machine. I was hoping I could do this: void descend() in { assert( depth != depth.max ); auto old_depth = depth; } out { // Note that I'm using a variable declared in the "in" contract. assert( depth == old_depth + 1 ); } body { ++depth; } The "old identifier" syntax seems nicer, though. I suppose the compiler could build a list of identifiers accessed that way, and save them at the end of the "in" contract. ++vote; -- Daniel
Jun 17 2007
parent reply Derek Parnell <derek psych.ward> writes:
On Sun, 17 Jun 2007 19:46:28 +1000, Daniel Keep wrote:

 Russ wrote:
 As far as I can tell, there is no "old" (as in Eiffel) for the function
postconditions, which makes them a lot less useful.  "Old" is an essential part
of DBC.  The postcondition contract often wants to talk about how the resulting
object is different from the original state of the object.  
 E.g. search for "old" on this page:
 http://archive.eiffel.com/doc/manuals/technology/contract/
 
 Here's a very simple example of what I want to do in D:
 
 void twiddleFoo(int direction, int amount)
 in
 {
     assert(direction == UP || direction == DOWN);
 }
 out
 {
     assert (direction == UP ? foo == old foo + amount : foo == old foo -
amount);
 }
 
 Is there away to achieve the effect of "old", i.e. for the "out" clause to
explicitly state that the value of "foo" has gone up or down by "amount"
according to the value of "direction"?  Am I not noticing something in D?

I found myself wanting something like this recently when I was writing a state machine. I was hoping I could do this: void descend() in { assert( depth != depth.max ); auto old_depth = depth; } out { // Note that I'm using a variable declared in the "in" contract. assert( depth == old_depth + 1 ); } body { ++depth; } The "old identifier" syntax seems nicer, though. I suppose the compiler could build a list of identifiers accessed that way, and save them at the end of the "in" contract. ++vote; -- Daniel

As a workaround idea ... alias typeof(depth) depth_T; depth_T descend() in { assert( depth != depth.max ); } out(old_depth) { // Note that I'm using a variable declared in the "in" contract. assert( depth == old_depth + 1 ); } body { depth_T old = depth; ++depth; return old; } int depth = 2; void main() { descend(); } -- Derek Parnell Melbourne, Australia "Justice for David Hicks!" skype: derek.j.parnell
Jun 17 2007
parent Russ Williams <digitalmars.D.learn russcon.removethispart.andthistoo.org> writes:
Derek Parnell Wrote:

 state machine.  I was hoping I could do this:
 
 void descend()
 in
 {
     assert( depth != depth.max );
     auto old_depth = depth;
 }
 out
 {
     // Note that I'm using a variable declared in the "in" contract.
     assert( depth == old_depth + 1 );
 }


 As a workaround idea ...
 
 alias typeof(depth) depth_T;
 
 depth_T descend()
 in
 {
     assert( depth != depth.max );
 }
 out(old_depth)
 {
     // Note that I'm using a variable declared in the "in" contract.
     assert( depth == old_depth + 1 );
 }
 body
 {
     depth_T old = depth;
     ++depth;
     return old;
 }

That workaround has the extremely unpleasant property of changing the function return type to return the old value, and becomes even more clunky when the contract mentions more than one field of "this", as often happens. E.g. in a game where you use resources to build stuff, you might have: void function buildStuff(int n) in { assert(0 <= n && n < resourceCount); } out { assert(resourceCount = old(resourceCount) - n); assert(stuffCount = old(stuffCount) + n); } Your workaround would have to change buildStuff to return a struct with 2 fields (the old resourceCount and the old stuffCount). Writing code like this would get very tedious very quickly. "old" is the sort of thing that you really need built-in language support for. It's an extremely useful part of DBC, and I'm quite surprised and disappointed to find it apparently missing from D. It's essential for defining the output contract of a function in any kind of useful serious way (as opposed to very simplistic "sanity checks" at function exit). I can imagine workarounds that involve writing code at function entry to explicitly clone "this" so that the out clause can use its values, and storing that clone as a global variable (yuck, and non-reentrant) or as part of every object (waste of space). But why should the programmer have to write such boilerplate code over and over? Without "old" postconditions are vastly less useful. It's analogous to other languages like C/C++/Java that only have plain old asserts but are sometimes claimed to support DBC, without having function preconditions/postconditions and class invariants.
Jun 17 2007
prev sibling next sibling parent reply Serg Kovrov <kovrov bugmenot.com> writes:
Russ wrote:
 As far as I can tell, there is no "old" (as in Eiffel) for the function
postconditions, which makes them a lot less useful.  "Old" is an essential part
of DBC.  The postcondition contract often wants to talk about how the resulting
object is different from the original state of the object.  
 E.g. search for "old" on this page:
 http://archive.eiffel.com/doc/manuals/technology/contract/

I have proposed some time ago that 'in' and 'out' could share same scope. That way it would be easy to achieve this (and more). Unfortunately, no one in NG were showing interest in it. -- serg.
Jun 17 2007
parent Russ Williams <digitalmars.D.learn russcon.removethispart.andthistoo.org> writes:
Serg Kovrov Wrote:

 As far as I can tell, there is no "old" (as in Eiffel) for the function
postconditions, which makes them a lot less useful.  "Old" is an essential part
of DBC.

I have proposed some time ago that 'in' and 'out' could share same scope. That way it would be easy to achieve this (and more). Unfortunately, no one in NG were showing interest in it.

That would certainly be an improvement... but it still forces the programmer to explicitly declare and initialize the various "old" variables - very repetitive common boilerplate code that should be automatically handled by the compiler (e.g. as in Eiffel) instead of explicitly appearing in the source code. http://digitalmars.com/d/cppdbc.html notes the drawbacks of making the programmer explicitly write a bunch of code for preconditions and postconditions in languages like C++ which don't have built-in support ... "By adding support for DbC into the language, D offers an easy way to use DbC and get it right." The exact same argument holds for "old" in the postconditions, which very often need to refer to the starting value of "this" to be useful.
Jun 17 2007
prev sibling next sibling parent reply Manfred Nowak <svv1999 hotmail.com> writes:
Russ wrote

 E.g. search for "old" on this page:
 http://archive.eiffel.com/doc/manuals/technology/contract/

This is an archived file. Is Eiffel really capable of for example holding complete arbitrary "old" databases for each recursive call of a modifying function? -manfred
Jun 17 2007
parent reply Russ Williams <digitalmars.D.learn russcon.removethispart.andthis.org> writes:
Manfred Nowak Wrote:

 Is Eiffel really capable of for example holding complete arbitrary 
 "old" databases for each recursive call of a modifying function?

It always worked fine for me. The compiler is essentially just saving the programmer from the repetitive error-prone tedium of explicitly writing the boilerplate code like "oldFoo = foo" to store the value at the start of the function call. If you are getting at the question of "What if foo is not a simple scalar value, but some complex linked structure which itself gets modified in the course of the function call?" then, yeah, it gets trickier. You need to talk about a clone of foo in the postcondition then. This may shed further light: http://www.faqs.org/faqs/eiffel-faq/ LOLD: What does the 'old' keyword mean? "The value of an Old expression old e is [...] the result that would have been produced by evaluation e just before the call's execution began." (ETL2, p.125). This is useful in postconditions. When using the keyword with a reference, it is clear from the definition that the value of "old a" will be the object to which 'a' referred at the beginning of the routine, and not the old value of the actual object. Obtaining a copy of 'a', if that is the required semantics, has to be done explicitly: ... old (clone (a)) ... This makes senses because copy and identity are issues with multiple solutions -- a shallow copy as done by 'clone' by default may not be enough for instance -- and a compiler cannot be reasonably expected to guess correctly which interpretation is appropriate for a given usage.
Jun 18 2007
parent reply Manfred Nowak <svv1999 hotmail.com> writes:
Russ Williams wrote

 This makes senses because copy and identity are issues 
 with multiple solutions -- a shallow copy as done by 
 'clone' by default may not be enough for instance -- and 
 a compiler cannot be reasonably expected to guess correctly 
 which interpretation is appropriate for a given usage.

Then `old' seems to control a preimplemented simplified memento pattern that is served once and only on function scope entry. So this seems an application for D's non existing scope guard `scope(entry)' In fact pre- and postconditions seem to be nothing else than blocks that are injected into the function body by `scope(entry)' and `scope (exit)' respectively. If this holds, then a call of the form `old variable' can in principle be seen as the duality of scope(entry){ save( variable);} injected into the function body and the call `old variable' replaced by recall( variable); -manfred
Jun 18 2007
parent reply Russ Williams <digitalmars.D.learn russcon.removethispart.andthis.org> writes:
Manfred Nowak Wrote:
 So this seems an application for D's non existing scope guard
   `scope(entry)'

 In fact pre- and postconditions seem to be nothing else than blocks 
 that are injected into the function body by `scope(entry)' and `scope
 (exit)' respectively.

They are a little more than that since there are implications for inheritance (a precondition can be weakened in a derived class, and a postcondition can be strengthened in a derived class, which means OR-ing the preconditions of base.f() and derived.f() and AND-ing the postconditions). That inheritance aspect of DBC is defined in the language and done by the compiler so the programmer doesn't have to write boilerplate code to screw with it. Similarly "old" should be defined in the language. As it stands now, D discourages (to put it mildly) one from writing truly useful postconditions on functions which changes the object in a way dependent on the state of the object when the function is called. E.g. a container class might have a postcondition including the following assertion: void addFoo(Foo f) out { assert(fooCount = old(fooCount) + 1); } I really don't want to have to write some kind of extra boilerplate code to save the starting value of fooCount in order to express such simple postconditions.
Jun 18 2007
next sibling parent reply Deewiant <deewiant.doesnotlike.spam gmail.com> writes:
Russ Williams wrote:
 Manfred Nowak Wrote:
 In fact pre- and postconditions seem to be nothing else than blocks that
 are injected into the function body by `scope(entry)' and `scope (exit)'
 respectively.

They are a little more than that since there are implications for inheritance (a precondition can be weakened in a derived class, and a postcondition can be strengthened in a derived class, which means OR-ing the preconditions of base.f() and derived.f() and AND-ing the postconditions). That inheritance aspect of DBC is defined in the language and done by the compiler so the programmer doesn't have to write boilerplate code to screw with it.

Yeah, except: http://d.puremagic.com/issues/show_bug.cgi?id=302 -- Remove ".doesnotlike.spam" from the mail address.
Jun 18 2007
parent reply Russ Williams <digitalmars.D.learn russcon.removethispart.andthis.org> writes:
Deewiant Wrote:
 Yeah, except: http://d.puremagic.com/issues/show_bug.cgi?id=302

Hmm, that sucks. I start to get the feeling that DbC is not really taken seriously in D. :(
Jun 18 2007
parent Jari-Matti =?ISO-8859-1?Q?M=E4kel=E4?= <jmjmak utu.fi.invalid> writes:
Russ Williams wrote:

 Deewiant Wrote:
 Yeah, except: http://d.puremagic.com/issues/show_bug.cgi?id=302

Hmm, that sucks. I start to get the feeling that DbC is not really taken seriously in D. :(

I created a simple metaprogram that adds DbC inheritance and old objects: http://paste.dprogramming.com/dpu2y075.php It's just a temporary workaround - the syntax is bad and it does not parse all declarations nicely. Still, better than nothing :)
Jun 19 2007
prev sibling parent reply Manfred Nowak <svv1999 hotmail.com> writes:
Russ Williams wrote

 but if it means the programmer has to write explicit code to do
 it, that's not the good way to do it... 

I described how `old' might be implemented. You described that not being forced to write explicit code only holds in trivial cases. The non trivial cases need more work to be done. In terms of information hiding a construct like `old( clone( a))' seems horrible. So: 1) What is the right way to have a smooth transition from implicit to explicit coding? 2) Is explicit coding the `old' pattern even possible without breaking some OO-requirements? -manfred
Jun 18 2007
parent Russ Williams <digitalmars.D.learn russcon.removethispart.andthis.org> writes:
Manfred Nowak Wrote:
 I described how `old' might be implemented.
 
 You described that not being forced to write explicit code only holds 
 in trivial cases.

Those trivial cases are very common, however. In the nontrivial cases, the only explicit code would be needing to implement a clone or copy function for the type, which you quite often would already have anyway. In all cases, you should never have to write additional declarations inside the function just to support expressing what you need in the postcondition.
 The non trivial cases need more work to be done. In terms of 
 information hiding a construct like `old( clone( a))' seems horrible.

Well, ANY mention of private members in the postcondition violates information hiding; such portions of a postcondition would just be sanity checking for the implementer of the function presumably and ideally not displayed by tools that generate a public interface for human readers. But if there is a public function which returns some complex funky linked graph of objects, I don't see how "old(clone(funkyThing)) violates any kind of information hiding, given that funkyThing is publicly visible. The problem has been solved and implemented in other languages, e.g. Eiffel, and Lava (a language about which I know practically nothing else, but just found while googling for more info about "old" :) http://lavape.sourceforge.net/doc/html/DBC.htm
Jun 18 2007
prev sibling parent "Chris Miller" <chris dprogramming.com> writes:
On Sun, 17 Jun 2007 05:15:04 -0400, Russ  =

<digitalmars.D.learn russcon.removethispart.andthistoo.org> wrote:

 As far as I can tell, there is no "old" (as in Eiffel) for the functio=

 postconditions, which makes them a lot less useful.  "Old" is an  =

 essential part of DBC.  The postcondition contract often wants to talk=

 about how the resulting object is different from the original state of=

 the object.
 E.g. search for "old" on this page:
 http://archive.eiffel.com/doc/manuals/technology/contract/

 Here's a very simple example of what I want to do in D:

 void twiddleFoo(int direction, int amount)
 in
 {
     assert(direction =3D=3D UP || direction =3D=3D DOWN);
 }
 out
 {
     assert (direction =3D=3D UP ? foo =3D=3D old foo + amount : foo =3D=

 amount);
 }

 Is there away to achieve the effect of "old", i.e. for the "out" claus=

 to explicitly state that the value of "foo" has gone up or down by  =

 "amount" according to the value of "direction"?  Am I not noticing  =

 something in D?

Interesting. Perhaps amount.init could be used for the feature.
Jun 17 2007