D's design by contract is missing "old"?

[Derek Parnell]

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