Peter C. Chapin wrote:
> 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
You are not missing something, this is a known issue. It has been discussed
and I believe the intention was to do something about this, but with all the
high priorities I'm not sure when this will be solved.
As for the code that should not be compiled: this is easy to solve. If
unittests and contracts are to be compiled in for dmd, you need to pass the
-unittest flag to the compiler. This also sets the unittest flag, so you can
put the extra code in a version(unittest){} block which won't get compiled
without that flag (for a release).
Some compilers, like LDC, might make a distinction between unittests and
contracts (not sure exactly how). You could then also choose to put the
out() condition and supporting boilerplate code in a debug {} block instead.
In some situations this makes sense when you want your release to check
preconditions (caller violates the contract) but not postconditions (callee
violates the contract).
