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)'


I don't know about this nonexisting scope guard, but if it means the programmer
has to write explicit code to do it, that's not the good way to do it...


 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=


n  =


 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=


=3D old foo -  =


 amount);
 }

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


e  =


 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