Question about contracts on methods.

[Peter C. Chapin]

Hi!

I'm rather new to D and I'm experimenting with its support for 
contracts. I'm using dmd v1.51 on Windows.

Whenever I learn a new language I usually start by implementing a few 
"classic" components to get a feeling for how the language's features 
work in a pseudo-realistic setting. A class representing calendar dates 
is one of my favorite exercises. Here is a method next() of such a class 
that advances a Date to the next date on the calendar.

class Date {

    // etc...    

    void next()
    {
        if (day_m != days_in_month()) ++day_m;
        else {
            day_m = 1;
            if (month_m != 12) ++month_m;
            else {
                month_m = 1;
                ++year_m;
            }
        }
    }
}

The method days_in_month() is a private method in the class that returns 
the number of days in the "current" month. The fields day_m, month_m, 
and year_m are also private with the obvious meaning.

Okay, so far so good. Now I want to add a post condition on this method 
asserting that the date it computes is actually later than the original 
date. In my post condition I will need to access both the new values of 
day_m, month_m and year_m *and* the original values of those fields. 
There doesn't seem to be an easy way to do that.

I appreciate that I might need to explictly make my own copies of the 
original field values, but it seems like I can't do that locally in next
() because there is no place to declare the copies where they would be 
in scope in the post condition. Do I have to add three additional fields 
to the class itself and then copy the original values in the body of 
next()? Like this:

class Date {

    private {
        int original_day_m;
        int original_month_m;
        int original_year_m;
    }

    void next()
    out {
        assert(
            day_m > original_day_m ||
           (day_m == 1 && month_m > original_month_m) ||
           (day_m == 1 && month_m == 1 && year_m > original_year_m));
    }
    body {
        original_day_m   = day_m;
        original_month_m = month_m;
        original_year_m  = year_m;

        if (day_m != days_in_month()) ++day_m;
        else {
            day_m = 1;
            if (month_m != 12) ++month_m;
            else {
                month_m = 1;
                ++year_m;
            }
        }
    }
}

Not only does this seem awkward it has the disadvantage that there is 
now code related to the post conditions that won't be compiled out in 
the release build. Am I missing something? Surely this situation comes 
up often.

Peter