Code Contracts – A brilliant way to do validation in your code and even do more

Article
11/02/2010

In this post, I will try to introduce Code Contracts – a perfect way to implement, enforce validation and even do more in your code; C#. VB.NET or your language of choice. It is one the tools I keep in my “Development Mentoring Toolkit Bet”.

Fist lets start with the official introduction by “Microsoft Research” (https://research.microsoft.com/en-us/projects/contracts/).

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, post conditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.

Code Contracts bring the advantages of design-by-contract programming to all .NET programming languages.

I will try introduce the Code Contracts with a few examples (the language I have chosen is C# but remember Code Contracts is language-agnostic). We will try to enforce some validation of parameters before the execution of the logic as well as validation of the results after the execution of the code block. We will have write a console application where we utilize a manager class (PowerfulManager) that will act like a business tier object. In this manager class, we will see how to enforce some “contracts”. (To keep things simple, we will not example the console application but as you can easily guess, it will be an application that will create an instance of PowerfulManager and call the related functions.)

The PowerfulManager class will have a public property called UserId. We will first try to enforce that during the initialization of the class, a user id has to be provided which will be of type string. Our first rule will be to make sure that the provided user id parameter is not null or is not empty. Our class code would look something like below:

    1: public PowerfulManager(string userId)
    2:     : this()
    3: {
    4:     if (string.IsNullOrEmpty(userId))
    5:     {
    6:         throw new ArgumentException("userId");
    7:     }
    8:  
    9:     this.UserId = userId;
   10: }

With Code Contracts, the code above will be transformed into something like below:

    1: public PowerfulManager(string userId)
    2:     : this()
    3: {
    4:     Contract.Requires<ArgumentException>(!String.IsNullOrEmpty(userId), "userId");
    5:     this.UserId = userId;
    6: }

As you can see from the example above, we introduced the rule of userId parameter not being null or empty using the Contract.Requires static function.

Let’s now try to create a function that will take 2 integer parameters and return an integer result. The rules should be something like as follows:

minValue hould be greater or equal to 0
maxValue should be greater or equal to 0
minValue should be smaller than maxValue
The result should be smaller than maxValue

The original implementation would be something like this:

    1: public int DoSomething(int minValue, int maxValue)
    2: {
    3:     if (minValue >= 0)
    4:     {
    5:         throw new ArgumentException("minValue");
    6:     }
    7:  
    8:     if (maxValue >= 0)
    9:     {
   10:         throw new ArgumentException("minValue");
   11:     }
   12:     
   13:     if (!(minValue < maxValue))
   14:     {
   15:         throw new ArgumentException("minValue, maxValue");
   16:     }
   17:  
   18:     var result = maxValue - minValue;
   19:  
   20:     if (!(result <= maxValue))
   21:     {
   22:         throw new Exception("Something went wrong");
   23:     }
   24:  
   25:     return result;
   26: }

Now let’s see how this will can written using the Code Contracts.

    1: public int DoSomething(int minValue, int maxValue)
    2: {
    3:     Contract.Requires<ArgumentException>(minValue >= 0);
    4:     Contract.Requires<ArgumentException>(maxValue >= 0);
    5:     Contract.Requires<ArgumentException>(minValue < maxValue);
    6:  
    7:     Contract.Ensures(Contract.Result<int>() <= maxValue);
    8:  
    9:     return maxValue - minValue;
   10: }

I believe this is much neater, much more readable. Here we also see the “Contract.Ensures” method (line 7). This call allows us to define what should happen when we are returning from the function. As you can see in the code, we retrieve the value that we are returning using the Contract.Result method and check it against the maxValue.

Let’s now add one more function with the following logic and rules:

Let the function take two integer parameters and always return –1 after a successful run
Let’s set the class’s UserId property to “NewUserId”
As a rule, if we have to throw a BusinessException exception, we have to make sure we undo the UserId property to its old value
As a rule, when this function completes it’s execution, the UserId should never be null or empty

To simulate different possible scenarios, we will calculate maxValue modulus 4 and perform the following actions according to the value we get:

If value is 0, work as normal
If value is 1, throw a new Business Exception exception
If value is 2, first undo the change to the UserId property, then throw a new BusinessException exception
If value is 3, set the UserId property’s value to String.Empty

Now this is what the code will look like:

    1: public int DoSomethingElse(int minValue, int maxValue)
    2: {
    3:     Contract.EnsuresOnThrow<Exceptions.BusinessException>(Contract.OldValue<string>(this.UserId) == this.UserId, "UserId value is instable");
    4:     Contract.Ensures(!String.IsNullOrEmpty(this.UserId));
    5:  
    6:     var evaluationResult = maxValue % 4;
    7:  
    8:     var oldUserIdValue = this.UserId;
    9:  
   10:     this.UserId = "NewUserId";
   11:  
   12:     if (evaluationResult == 1)
   13:     {
   14:         throw new BusinessLogicLayer.Exceptions.BusinessException("Exception occured, I should undo the userId");
   15:     }
   16:  
   17:     if (evaluationResult == 2)
   18:     {
   19:         this.UserId = oldUserIdValue;
   20:         throw new BusinessLogicLayer.Exceptions.BusinessException("Exception occured, I should undo the userId");
   21:     }
   22:  
   23:     if (evaluationResult == 3)
   24:     {
   25:         this.UserId = String.Empty;
   26:     }
   27:  
   28:     return -1;
   29: }

At like 3, we define a rule saying that if BusinessException is thrown, old value of UserId property should be the same as the current value of UserId (in other words, any changes done to the UserId property should be undone). At Line 4, we define a rule where we say that, no matter what, when the function completes, UserId property should not be null or empty.

I find “Code Contract” fascinating, fun to use and great to experiment with. The examples I have provided above are just simple examples of what you can do with them. If you read the documentation (the documentation is over explanatory), you will see that there are a great number of more functionality provided such as Contract.ForAll, Interface Contracts and Object Invariants.

Object Invariants is a great feature where you can define what conditions that should hold true on each instance of a class whenever that object is visible to a client. Literally, you can enforce the object to be in a “valid” or “good” state. Depending on the feedback, I may try to provide some examples around Object Invariants.

Code Contracts – A brilliant way to do validation in your code and even do more

Additional resources