LA.NET [EN]

Nov 05

Yesterday I was really excited after finding out that we’ll finally have a library for performing Design By Contract verifications on our code. Ok, the runtime validations could already be simulated by writing some code (I’ve already written several helpers classes in my current applications), but the truth is that the Code Contracts library adds static verification and will enable you to catch several errors during compilation. I believe this is more than enough for you to be interested in this new library, right?

Ok, so lets start with a basic scenario which will let me illustrate the usage of the existing static methods available on the CodeContract class (attention: do notice that this class will be renamed into Contract on the final release): lets suppose we have a simple class called student which looks like this:

public class Student
{
        private String _firstName = "";
        private String _lastName = ""; 
        public Student(Int32 studentId)
        {
            StudentId = studentId;
        } 
        public Int32 StudentId { get; private set; } 
        public String FirstName { get { return _firstName; } } 
        public String LastName { get { return _lastName; } } 
        public void ChangeName(String firstName, String lastName)
        {
            _firstName = firstName;
            _lastName = lastName;
        } 
}

One of the things you’ll want to apply to your methods are preconditions for checking parameter values. For instance, lets assume that only positive integers are valid for student ids. So, if you try to run the following code:

var std = new Student( –1 );

You should get an error at runtime. If you use a precondition, you’ll also get a compile warning (yes, you’ve read it correctly: *compile* warning). Here’s what you need to do to achieve that:

public Student(Int32 studentId) {
   CodeContract.Requires(studentId > 0);
   StudentId = studentId;

Btw, the CodeContract class is defined on the System.Diagnostics.Contracts namespace. Besides simple conditions, you can also,for example,call pure methods. A pure method is annotated with the PureAttribute and when you do that, you’re actually saying that the method doesn’t produce any side effects (using methods might give you false positives too!).

Besides your own methods, you can also access property getters, operators and several methods whose qualified name begins with System.String, System.IO.Path, System.Type and, of course, CodeContract methods. Do notice that whenever you access another member, you’ll have to make sure that that member has at least the same visibility as the method where you’re adding your contracts.

One more note: when you install the code contract bits, your projects will get an additional tab on the property page which you’ll have to configure for having static and runtime analysis. Not setting the checkboxes means that you won’t have either of those validations.

Besides checking  values, you can also give some guarantees regarding the state of your object after your method ends. For instance, in the previous example you can say that when the constructor does its job, you’ll always have a positive ID. Here’s how you can do that:

public Student(Int32 studentId) {
  CodeContract.Requires(studentId > 0 );
  CodeContract.Ensures(StudentId > 0);
  StudentId = studentId;
}

You can also ensure state when you get an exception. You do this by calling EnsuresOnThrow generic method. When you do this, you’re saying that even if you get an exception, the predicate you specify should be met.

You can also use invariants. Invariants define conditions under which an object is in a good state. By adding an invariant, you’re defining a group of predicates that will always be run after all your public method calls. An invariant is defined through a protected method which only contains several Ensures method calls. For instance, if we think that ensuring that the StudentId is always positive is really necessary for guaranteeing the good state of our instances of Student, then we can add a method that looks like this to our class:

[ContractInvariantMethod]
protected void ObjectInvariant() {
    CodeContract.Ensures(StudentId > 0);       
}

And now, whenever someone calls a public method of your class, the previous validation will always be performed. And that’s it for today. Tomorrow we’ll keep talking about code contracts. Keep tuned.

1 comment so far

  1. Vladekk
    1:52 pm - 11-6-2008

    Neat, Spec# transformed to something usable and understandable for casual programmers 😉