Like this article? We recommend
Like this article? We recommend
Like this article? We recommend
Using Code Contracts
If you consider the guard statements to describe a set of assumptions about the input, it is reasonable to say that these assumptions describe a contract that the method satisfies. You could further say that these assumptions are actually pre-conditions that must be satisfied before the Calculate method will execute.
Listing 4 shows the same Calculate method using code contracts rather than guard statements. The intent described by the contracts is much clearer than that described by the guard statements. In addition, the logic used by the code contract statements matches the way it is described in the business logic.
Listing 4—Code Contracts
public int Calculate(int divisor, int dividend)
{
Contract.Requires(divisor > 0);
Contract.Requires(dividend > 0);
Contract.Requires(divisor > dividend);
return dividend / divisor;
}
If this version of the Calculate method was contained in a class named Test and used by the code in Listing 5, the code contract tools would generate the warnings shown in Figure 4 if Perform Static Contract Checking was enabled.
Listing 5—Calling Code that Violates a Contract
class Program
{
static void Main(string[] args)
{
Test t = new Test();
t.Calculate(0, 0);
}
}
){kind=small}
Figure 4 Compile-time contract violations
Pre-Conditions
Pre-conditions help answer the question of what input is expected. They are contracts about the input when the method is invoked and are most commonly used to validate parameter values.
Listing 5 showed an example of pre-conditions using one of the Contract.Requires overloads. If you are replacing legacy code that had already documented exceptions for invalid inputs, such as code that used legacy guard statements, you may want to continue throwing those exceptions but still utilize code contracts. You can use one of the generic Contract.Requires<T> overloads as shown in Listing 6 to accomplish this.
Listing 6—Using Contract.Requires<T>
public int Calculate(int divisor, int dividend)
{
Contract.Requires<ArgumentOutOfRangeException>(divisor > 0, "divisor");
Contract.Requires<ArgumentOutOfRangeException>(dividend > 0, "divisor");
Contract.Requires<ArgumentException>(divisor > dividend, "divisor");
return dividend / divisor;
}
The result of running this version of the Calculate method with the same calling code from Listing 5 is shown in Figure 5.
){kind=small}
Figure 5 Runtime contract violations
When using either version of Contract.Requires, all of the members specified by the pre-condition must be at least as accessible as the method itself. This means that a private field couldn't be specified in a pre-condition for a public method because callers would have no way of validating such a contract before calling the method.
In addition, the condition should be free of side effects. This applies to any methods that are called within a contract as well. Such side-effect free methods are also called pure methods and must not update any pre-existing state; they can, however, modify objects created after the pure method has begun executing.
Currently, the following are assumed to be pure:
- Methods marked with the Pure attribute. When a type is marked with the Pure attribute, all methods in that type are considered to also be marked with the Pure attribute.
- Property get accessors
- Operators
- Any method whose fully qualified name begins with System.Diagnostics.Contracts.Contract, System.String, System.IO.Path, or System.Type
- Any invoked delegate if the delegate type itself is marked with the Pure attribute. The System.Predicate<T> and System.Comparison<T> delegates are considered pure.
Post-Conditions
If pre-conditions help answer the question of what input is expected, post-conditions help answer the question of what output is expected. They are contracts about the state of a method when it terminates, and are checked just prior to exiting the method. Post-conditions may specify members that are less accessible than the method itself. This means that a private field could be specified in a post-condition for a public method.
Most post-conditions will be specified using one of the Contract.Ensures overloads, and specify a condition that must be true when the method completes normally. Listing 7 shows an example of using a post-condition to ensure the result of the division operation is non-zero.
Listing 7—Using Post-Conditions
public int Calculate(int divisor, int dividend)
{
int result = 0;
Contract.Requires<ArgumentOutOfRangeException>(divisor > 0, "divisor");
Contract.Requires<ArgumentOutOfRangeException>(dividend > 0, "divisor");
Contract.Requires<ArgumentException>(divisor > dividend, "divisor");
Contract.Ensures(result != 0);
result = dividend / divisor;
return result;
}
In order to write this post-condition, it was necessary to change the implementation so the result of the division was captured in a local variable. Because this isn't always practical, the code contracts library provides the Contract.Result<T> method to refer to the actual return value. Using Contract.Result<T> would allow the Calculate method to be written as shown in Listing 8.
Listing 8—Using Post-Conditions and Contract.Result<T>
public int Calculate(int divisor, int dividend)
{
Contract.Requires<ArgumentOutOfRangeException>(divisor > 0, "divisor");
Contract.Requires<ArgumentOutOfRangeException>(dividend > 0, "divisor");
Contract.Requires<ArgumentException>(divisor > dividend, "divisor");
Contract.Ensures(Contract.Result<int>() != 0);
return dividend / divisor;
}
If you need to write a post-condition that references an out parameter, you must use the Contract.ValueAtReturn<T> method instead of Contract.Result<T>.
Just as you can refer to method return values and out parameters, it is also possible to refer to the original value of an expression from the pre-condition state using Contract.OldValue<T>. There are, however, several restrictions:
- The old expression may only be used in a post-condition.
- An old expression cannot refer to another old expression.
- The old expression must refer to a value that existed in the method's pre-state.
Object Invariants
Sometimes it is necessary to specify a condition that should be true on each instance of a class. In other words, it defines a set of conditions that must be true both before and after an operation; therefore, invariants express the conditions that are required for the object to be in a "good" state.
Specifying object invariants is done using an invariant method. This is simply a method that satisfies the following rules:
- It has private accessibility.
- It has a void return type.
- It is marked with the ContractInvariantMethod attribute.
- It contains only calls to the Contract.Invariant method.
While the name of the method is not meaningful, a best practice is to name it something meaningful like ObjectInvariants or just Invariants. It is also possible to specify more than one method for the object invariants, although you should probably keep it to just one method for ease of maintenance.
Changing the Calculate method to the code shown in Listing 9 so that it is part of a larger class which uses object invariants allows you to write a class that ensures the value of result is always not equal to zero.
Listing 9—Using Object Invariants
public class Test
{
private int result = 0;
public int Calculate(int divisor, int dividend)
{
Contract.Requires<ArgumentOutOfRangeException>(divisor > 0, "divisor");
Contract.Requires<ArgumentOutOfRangeException>(dividend > 0, "divisor");
Contract.Requires<ArgumentException>(divisor > dividend, "divisor");
Contract.Ensures(Contract.Result<int>() != 0);
this.result = dividend / divisor;
return result;
}
[ContractInvariantMethod]
private void Invariants()
{
Contract.Invariant(this.result != 0);
}
}
Quantifiers
Code contracts offer support for quantifying a condition through the ForAll and Exists methods. To specify a condition is true for all elements in a collection, you should use the ForAll method. The Exists method determines if any element satisfies the condition.
Both of these methods have two overloads. One overload is generic and takes a collection and a predicate representing the method that will be applied to each element in the collection. The second overload is not generic and takes an inclusive lower bound, an exclusive upper bound, and a predicate representing a method that must take an integer as its argument. Listing 10 shows some examples of using quantifiers.
Listing 10—Using Quantifiers
public int Foo<T>(IEnumerable<T> xs)
{
Contract.Requires(Contract.ForAll(xs, x => x != null));
return default(int);
}
public int[] Bar()
{
Contract.Ensures(Contract.ForAll(0, Contract.Result<int[]>().Length,
index => Contract.Result<int[]>()[index] > 0));
return default(int[]);
}