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
