LA.NET [EN]

Nov 06

Today I’ll keep writing about the new Code Contracts framework and we’ll see how we can use the write contracts that validate method return values and “old” values. Lets start with method return values…

As you might expect, you’re able to refer to return values on your postconditions. To show you the kind of thing you’ll be writing, we will start by changing the class we presented yesterday and we’ll add a BirthDate property to it:

class Student{

private DateTime _birthDate;
public DateTime BirthDate {
            get { return _birthDate; }
            set {
                CodeContract.Requires(value> new DateTime(1900, 1, 1));
                _birthDate = value;
            }
  } 
}

Now, we can calculate the age by adding a new method called CalculateAge to this class. This probably is a good way to implement it:

class Student{
  public Int32 CalculateAge()  {
            var currentDate = DateTime.Now;
            var years = currentDate.Year – _birthDate.Year;
            if( currentDate.CompareTo(_birthDate.AddYears(years)) < 0 )
            {
                years–;
            }
            return years;
   }
}

Ok, so one of the things we can do is make sure that we return a valid age. Just to be sure, we can say that the age of a person must always be bigger than 0, so we’ll go ahead and add that condition:

public Int32 CalculateAge()  {
        CodeContract.Ensures( CodeContract.Result<Int32>() > 0 );
        //previous code
}

The CodeContract.Result<T> method is generic and can only be called inside the Ensures method. T should be replaced by the return type of the method.

Besides specifying the contract for the return value, you can also use another special method: CodeContract.OldValue<T>. This method expects a parameter of type T and there are several restrictions which apply to the values that can be passed to it. For instance, the return value (CodeContract.Result<T>) cannot be used on the expression passed to that parameter. You can’t also use out parameters either! The docs contain full list with these rules, so I won’t be putting them here. Instead,I’ll show how you can apply these method in your code.

One of the things you can do is guarantee that you’ll only update the value of the field _birthDate if the new date is different than the existing one. You can also specify this with a contract.Here’s an example (ok,sorry for the lame example, but I’m a little but tired today:)):

public DateTime BirthDate {
   get { return _birthDate; }
   set {
     CodeContract.Requires(value > new DateTime(1900, 1, 1));
     CodeContract.Ensures(
            CodeContract.OldValue(_birthDate) != _birthDate);
      _birthDate = value;
   }
}

Ok, this should be enough for showing you how you can use the OldValue method. So, if you try to write this code:

var st = new Student(2);
st.BirthDate = new DateTime(1976, 6, 27);
//more code here…
st.BirthDate = new DateTime(1976, 6, 27);

You’ll surely get an assert at runtime (on the next posts, we’ll see how easy it is to replace the assert with, say, an exception – which is something I really prefer). And that is it for today, As I said earlier, the examples might not have been the best, but I think that they were enough for illustrating the usage of return methods and old values in your contracts. On the next post, we’ll keep looking at this framework and see how you can use non-public fields and out parameters in your contracts. Keep tuned!

Leave a Reply

Your email address will not be published. Required fields are marked *


*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>