Note: This blog post transferred from my OLD BLOG and was originally posted in 2008.
As part of making the .Net framework fully support Design by Contract approaches, the BCL team along with the CLR team had integrated very powerful project from Microsoft Research (MSR) named Code Contracts, and what code contracts do for you as giving you declarative, integrated, and easy way to express all the facts you already know about your program by design to make it work better.
Before you used to do that using Assert statements or even using some comments on top of your API telling people what’s the rules they should follow in order to perfectly use your Methods, one major thing about those methods that it wasn’t a Must to Follow, on the contrary Code Contracts is enforcing and checked statically at compile time and dynamically at runtime.
| Note: At this CTP build of Visual Studio and .Net Framework, the Static Analysis tools is not supported yet, but the dynamic runtime checking is supported
Microsoft decided to provide Code Contracts as Library Solution instead of Language Solution that’s to make them widely used by all the languages using .Net framework, So new in .Net Framework 4.0 BCL under System.Diagnostics.Contracts you will find the code contracts library. All Code contracts grouped under CodeContract static Class as Static Methods that return void, each Contract Methods has 2 overloads; One takes a Boolean expression that must be true in order for contract to be valid and another overload that take expression and a message to display in case of contract violation, things you should know about contracts:
|
 |
How to use Contracts
Defining contracts is fairly easy as adding couple of checking lines at the start of the method, check the following sample calculator class to understand how you can use contracts inside your classes:
1: public class Calculator
2: {
3: /// <summary>
4: /// Adds 2 numbers
5: /// </summary>
6: /// <param name="x">First number can't be zero</param>
7: /// <param name="y">Second number can't be zero</param>
8: /// <returns>Sum of the 2 numbers</returns>
9: public int Add(int x, int y)
10: {
11: CodeContract.Requires(x > 0 && y > 0);
12:
13: return x + y;
14: }
15:
16: /// <summary>
17: /// Subtract 2 positive numbers
18: /// </summary>
19: /// <param name="x">First Number must be larger than the second</param>
20: /// <param name="y">Second number</param>
21: /// <returns>Result of subtraction, can't be negative</returns>
22: public int Sub(int x, int y)
23: {
24: CodeContract.Requires(x > y);
25: CodeContract.Ensures(CodeContract.Result<int>() > -1);
26:
27: return x - y;
28: }
29: }
Types of Contracts
CodeContracts has 3 main types:
1. Preconditions
Use them to validate your method parameters, they must be true at method entry for successful execution of the method. It’s the responsibility of the caller to make sure these conditions are met.
- CodeContract.Requires(x>= 0);
- CodeContract.RequiresAlways(x>= 0);
The difference between Requires and RequiresAlways is the last one always included even in release builds, so you can use it for contracts that you want to include in your release.
2. Postconditions
They are declared at the beginning of a method, just like preconditions. The tools take care of checking them at the right times.their jobs is to ensure that methods has successful closure.
- CodeContract.Ensures(z != null); // must be true if method closes successfully
- CodeContract.EnsuresOnThrow<IOException>(z != null); // Grantuee some variable status in case of specific exceptions.
Also it is very often necessary to refer to certain values in postconditions, such as the result of the method, or the value of a variable at method entry. CodeContract class allow this using some special referral methods; they are valid only in a postcondition.
- CodeContract.Ensures(CodeContract.Result<Int32>() >= 0); //represents the value results from a method
- CodeContract.Ensures(x > CodeContract.OldValue(x)); // represents the value as it was at the start of the method or property. It captures the pre-call value in a shallow copy.
3. Object Invariants
They are contracts that must be true at all public methods exists in an object. They are contained in a separate method that is marked with the ContractInvariantMethodAttribute. The method must be parameter-less and return void. That method contains some number of calls to the CodeContract.Invariant method.
[ContractInvariantMethod]
void ObjectInvariant() {
CodeContract.Invariant(someData >= 0);
}
What do you ship?
 |
The final question that matters is what I’ll deliver the customer, in reality Code contracts has a very intelligent way of generating its own contract assemblies, so you have your old normal .net assemblies without contract that you can release to your customers and don’t worry about the performance hit, and another assembly contains the contracts only without any code; you can deliver those assemblies to your customer that you want them have the same code checking experience you have during compile time. |
More Information:
- Microsoft Research’s code contracts website.
- PDC 2008: PC49, Microsoft .NET Framework – CLR Futures (Video|PPTX).
- PBC 2008: TL51 Research: Contract Checking and Automated Test Generation with Pex (Video|PPTX).
- Introduction to Code Contracts [Melitta Andersen].
Related Articles:
- CLR 4.0: Type Embedding.
- CLR 4.0: New Enhancements in the Garbage Collection
- CLR 4.0: Corrupted State Exceptions
Hope this Helps,
Ahmed
eknowledger 