Home » .NET Framework » Code Contracts – Postconditions and Preconditions

Code Contracts – Postconditions and Preconditions

Code contracts, which were introduced in .NET Framework 4.0, enable a developer to publish various conditions that are necessary within an application. They can be installed through the Visual Studio Gallery.  Code contracts involve the following:

• Preconditions – Conditions that have to be fulfilled before a method can execute
• Invariants – Conditions that do not change during the execution of a method
• Postconditions – Conditions that that are verified upon completion of the method

Using code contracts requires a different approach for managing exception flow within an application. Some code you ordinarily write, such as ensuring that a returned object is not null, will be handled in the method for you by the code contract. Rather than validating everything that is returned from a method call, you ensure that everything entering and leaving your methods are correct.  This is a fundamental shift in how a lot of classic applications are written as the basis of trust moves into the method that is being called.  This means that validation of the returned value does not need to be carried out in the calling method.

Before code contracts, a standard way to manage validation within a method was to perform a validation check, throwing an ArgumentException when a particular parameter is invalid. This is shown below:

internal Article GetArticle(int id)
{
if (id <= 0) { throw new ArgumentException("id"); }
// some work here
}

This code checks to ensure that the incoming argument is greater than 0 to represent a valid Id. If the code determines that the value is incorrect, it throws an ArgumentException with the name of the parameter that failed. Using contracts to perform this check enables consumers of the methods to get some information about the expectations of the method. The code below provides both Preconditions (Requires) and Postconditions (Ensures).

internal Article GetArticle(int id)
{
System.Diagnostics.Contracts.Contract.Requires(id > 0);
System.Diagnostics.Contracts.Contract.Ensures(Contract.Results() != null);
// some work here
}

This is powerful because it provides you the ability to get more distinct information directly from the debugger as shown below.

CodeContractDebugger

Not only does the use of Code Contracts provide a more accurate message when the validation fails, it also provides constant messaging as to what the contracts expect, as demonstrated in the screenshot below that demonstrates the messages created during the build process.

CodeContractMessages

You can trap these kinds of errors as needed as well as get detailed information about the validation issues.  Precondition and postcondition contracts are straightforward and concern themselves with incoming parameters and the return value of the method, respectively.  Invariants are a different breed, as they are concerned with the lifetime of the object.  Using invariant contracts are the subject of the next post.

About these ads

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s