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

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

Lutger <lutger.blijdestijn@gmail.com> wrote in news:hescc2$161$1@digitalmars.com:

> 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.

Okay, thanks for the information. It occurs to me that one way to solve this problem would be to allow declarations in the precondition be visible in the post condition. Then one could do something like

    void next()
    in {
        int original_day_m   = day_m;
        int original_month_m = month_m;
        int original_year_m  = year_m;
    }
    out {
        assert( ... expression using original_day_m, etc ... )
    }
    body {
      // No code related to pre or post conditions.
    }

This might not be an ideal resolution but it seems a lot better than the current situation and it doesn't look like it would be too hard to implement (but what do I know!).


> As for the code that should not be compiled: this is easy to solve...

Thanks for your suggestions!

Peter

Peter C. Chapin wrote:
> Lutger <lutger.blijdestijn@gmail.com> wrote in
> news:hescc2$161$1@digitalmars.com: 
> 
>> 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. 
> 
> Okay, thanks for the information. It occurs to me that one way to solve this problem would be to allow declarations in the precondition be visible in the post condition. Then one could do something like
> 
>     void next()
>     in {
>         int original_day_m   = day_m;
>         int original_month_m = month_m;
>         int original_year_m  = year_m;
>     }
>     out {
>         assert( ... expression using original_day_m, etc ... )
>     }
>     body {
>       // No code related to pre or post conditions.
>     }
> 
> This might not be an ideal resolution but it seems a lot better than the current situation and it doesn't look like it would be too hard to implement (but what do I know!).

The problem is, where do those variables get stored? The function body will overwrite anything that's left on the stack.
At the moment, AFAIK the only way to do this at present is to write the contracts as nested functions.

void next()
{
     int original_day_m;
     int original_month_m;
     int original_year_m;
    void inContract() { original_day_m = day_m; ...}
    inContract();
    void outContract() { assert( ... expression using original_day_m, etc ... ) }

    // body...
   outContract();
   return;
}

Don <nospam@nospam.com> wrote in news:hf0obf$1th8$1@digitalmars.com:

>>     void next()
>>     in {
>>         int original_day_m   = day_m;
>>         int original_month_m = month_m;
>>         int original_year_m  = year_m;
>>     }
>>     out {
>>         assert( ... expression using original_day_m, etc ... )
>>     }
>>     body {
>>       // No code related to pre or post conditions.
>>     }
>> 
>> This might not be an ideal resolution but it seems a lot better than the current situation and it doesn't look like it would be too hard to implement (but what do I know!).
> 
> The problem is, where do those variables get stored? The function body will overwrite anything that's left on the stack.

Couldn't the compiler just translate the above into something similar to your example using nested functions?

Peter