In the first part of this series, I wrote about how you can check preconditions with Code Contracts. We also looked at some of the features of postconditions. In this post, we will implement postconditions with an example and go on to look at object invariants.
You can implement Postconditions using Contract.Ensures method. Similar to the Contract.Requires, this takes in a boolean parameter and can display a string as the error message. Unlike the Requires method, Contract.Ensures cannot throw a specific exception.
We will use the same Concatenate method that we kicked off in the first part and enhance that with some postconditions checks. Here is what it looks like
1: static string Concatenate(string leadingstring, string trailingstring)
2: { 3:
4: //raise an exception if the contract fails
5: Contract.Requires<ArgumentNullException>(leadingstring.Length > 0);
6: //make sure the string is greater than 10 characters before the code exits the method
7: Contract.Ensures(Contract.Result<string>().Length > 10, "The string is too short");
8: //ensure that the concatenated string is at least longer than the leading string by 2
9: Contract.Ensures(Contract.Result<string>().Length > Contract.OldValue<string>(leadingstring).Length + 2, "The value of the concatenated string is not long enough");
10: leadingstring = String.Concat(leadingstring, trailingstring)
11: return leadingstring;
12: }
The method now returns the concatenated string. It also includes a couple of ensures statements. Note that though we are implementing postconditions, the Contract.Ensures statement should be included at the beginning of the method and not at the end. There are two checks I have done
The first to make sure that the length of the concatenated string is greater than 10. The Contract.Result returns the value that is being returned from the method.
The second check makes sure that the concatenated string is at least 2 characters longer than the leading string. Here, I have used the Contract.OldValue to get the original value of leadingstring when it entered the method.
Unlike Contract.Requires, you will not be able to catch a specific exception if the Contract.Ensures fails. In the main method, I have caught a generic exception to handle any contract exceptions. Below is my main method with the changes.
1: static void Main(string[] args)
2: { 3: try
4: { 5: string resultString = Concatenate("1234567891011", "a"); 6: Console.WriteLine("The result is {0}", resultString); 7: Console.WriteLine(resultString);
8:
9: }
10: //catch the argument null exception raised by the contract
11: catch (ArgumentNullException nullString)
12: { 13: Console.WriteLine(nullString.Message);
14: }
15: catch (Exception ex)
16: { 17: Console.WriteLine(ex.Message);
18: }
19:
20: Console.ReadLine();
21: }
Object InvariantsInvariants are code contract features that enable you to check object state and ensure conditions are met when you call methods on these objects. To validate a class using invariants, you will have to write an Invariant method that returns void. This method needs to be decorated with the [ContractInvariantMethod] attribute.
To demonstrate the use of invariants, I have refactored the above concatenation code using an external class called StringManipulation. This class that has two public variables and one Concatenate method.
1: using System;
2: using System.Collections.Generic;
3: using System.Linq;
4: using System.Text;
5: using System.Diagnostics.Contracts;
6:
7: namespace CodeContractsSample
8: { 9:
10: class StringManipulation
11: { 12: public string leadingString = "12345678";
13: public string trailingString = "87654321";
14:
15: [ContractInvariantMethod]
16: protected void ObjectInvariant()
17: { 18: Contract.Invariant(this.leadingString.Length>5);
19: Contract.Invariant(this.trailingString.Length>5);
20:
21: }
22:
23: public string Concatenate()
24: { 25: return String.Concat(leadingString, trailingString);
26: }
27:
28: }
29: }
As you can see, I have also added the CodeInvariant method to check if both the strings are at least 5 characters in length. This means that I will have to initialize the string to pass that condition. Otherwise the object does not get created.
The other consideration you will have to keep in mind when using object invariants are that the invariant checks are only done when a method call is made. In essence, invariants will not work for DTO or DataContracts. The workaround is to use Contract.Requires on the property.
Legacy If..Else Blocks
While Code Contracts are a new .NET 4.0 feature, there exists a lot of legacy code using If…Else… that does similar validations. If you want the .NET framework to treat them as contracts, you can use the EndContractBlock provided the If…Else… are the first set of statements in a method. when you use EndContractBlock, all the If..Else.. conditions are assumed as preconditions.
Code Contract Usage Considerations
Code Contracts give dev leads and architects a plethora of options to do validations. But, as with anything else, there are certain decision points that need to be taken care of.
Decide very early in the project how you are going to use Code Contracts. Though static checking is very powerful, it also puts a lot of drab in your build process. Make sure you are turning static checking on only when you need it.
You could also do runtime checking only on debug builds. This works very well for TDD projects
Be wary of turning on runtime checking on production builds. Remember, .NET 4.0 is still in its beta.
Code Contracts are very extensive. Make sure you understand all the features offered before picking on the best way to do your validations or checks.
When you are using both preconditions and postconditions in the same method, there is a specific order which is recommended. The order according to the Code Contract documentation is as follows
Legacy if…Then…Else blocks
Contract.Requires to check public preconditions
Contract.Ensures to check public postconditions
Contract.EnsuresOnThrow to check public exceptional conditions
Contract.Ensures to check all private postconditions
- Contract.EnsuresOnThrow to check all private postconditions before finishing off with the EndContractBlock
You can use Contracts with pre .NET 4.0 versions by referencing the Microsoft.Contracts library. In .NET 4.0 Code Contracts have been integrated into the mscorlib.dll
One of the recommended ways of using Code Contracts is to have a separate config file for contracts.
- The contracts build output can be shipped along with your build so that other developers\administrators can make use of it. Make sure you understand the different build options.
That concludes my two part post on Code Contracts and their usage. The posts try to give you a peek are by no means exhaustive on the features that Code Contracts offer. For complete understanding, I would recommend you download the manual from DevLabs and give it at least a quick skim through. Happy Coding!!!!
