www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.learn - Question about contracts on methods.

reply "Peter C. Chapin" <pcc482719 gmail.com> writes:
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
Nov 28 2009
parent reply Lutger <lutger.blijdestijn gmail.com> writes:
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).
Nov 28 2009
parent reply "Peter C. Chapin" <pcc482719 gmail.com> writes:
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
Nov 28 2009
parent reply Don <nospam nospam.com> writes:
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;
}
Nov 30 2009
parent "Peter C. Chapin" <pcc482719 gmail.com> writes:
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
Nov 30 2009