Derik Whittaker



Code Contracts Primer – Part 4: Utilizing Pre & Post Conditions

If you are not familiar with the Code Contracts library which is coming out of Microsoft R&D labs, you need to check this pretty cool little library out.  As of Vs2010/.Net 4.0 this library will be making the jump out of the R&D labs. 

Over the next few blog posts we will be taking a look at the topics below.

In this post we are going to take a look at what might be considered the most basic usage scenario for the contracts library, Pre and Post condition validation.

What is a pre-condition validation?
This is when we want to validate the state of the world (parameters or other state holding values) is valid prior to running a method.  Pre-condition validation is done by utilizing the Contract.Requires(…) or Contract.Requires<CustomExceptionHere>(…) method.

The code below is what your pre-condition code could look like the code below:

public ReportCard GetDailyReportCard(Int32 employeeId, DateTime dateForReportCard)
	Contract.Requires(employeeId > 0);
	Contract.Requires<ArgumentOutOfRangeException>(dateForReportCard.Date == DateTime.Now.Date);
// do something meaning var reportCard = new ReportCard(employeeId); return reportCard; }

The code above shows 2 different ways you can use the contracts libray.  The first simply uses the standard .Requires() logic and is meant to ensure that the employeeId is always > 0.  The second uses the overload of .Requires<>() and will provide the exception type which should be thrown if a contract is violated. As we have mentioned before, the contracts library uses Code Weaving to do its magic.  Lets take a look at how it re-wrote the .Requires() for us on the back end (via reflector).

public ReportCard GetDailyReportCard(int employeeId, DateTime dateForReportCard)
	if (__ContractsRuntime.insideContractEvaluation <= 4)
			__ContractsRuntime.Requires(employeeId > 0, null, "employeeId > 0");
			__ContractsRuntime.Requires(dateForReportCard.Date == DateTime.Now.Date, null, "dateForReportCard.Date == DateTime.Now.Date");
	return new ReportCard(employeeId);

As you can see the code has changed, but not too much.

Now that we have mastered pre-conditions it is time to take a look at post-conditions

What is a post-condition validation?
This is when you want to validate the state of a method when that method terminates.  With post conditions you can assert that the return value so the caller can be assured the values will always be within range when returned.  Post-Condition checks can be done with the Contract.Ensures() method and can take a special command which is Contract.Result<> which allows you to specify the result type and its condition.

The code below is an simple example of how you can create your post-condition check.

public ReportCard GetWeeklyReportCard( Int32 employeeId )
	Contract.Ensures( Contract.Result<ReportCard>() != null );
	var reportCard = new ReportCard( employeeId );
	return reportCard;           

In the check above we are simply trying to ensure that the return value from this method will never be null.  Of course this is just a simple example and you could validate over types of items as well.

As we did in the pre-condition, lets take a look at the code as it exists after code weaving:

public ReportCard GetWeeklyReportCard(int employeeId)
	ReportCard reportCard = new ReportCard(employeeId);
	ReportCard CS$1$0000 = reportCard;
	ReportCard Contract.Result() = CS$1$0000;
	if (__ContractsRuntime.insideContractEvaluation <= 4)
			__ContractsRuntime.Ensures(Contract.Result() != null, null, "Contract.Result() != null");

	return Contract.Result();

Again you can see that the weaver did its magic, but this time it did a bit more work.  The good news for us is that the code still works as intended so there is nothing too much to worry about.

Now that we have taking a look at both pre-conditions and post-condition checking with the contracts library you are more than on your way to utilizing this library in your code.

Till next time,

Posted 06-15-2009 2:29 PM by Derik Whittaker
Filed under: ,



Tim Haynes wrote re: Code Contracts Primer – Part 4: Utilizing Pre & Post Conditions
on 06-16-2009 10:04 AM

I love this little Code Contracts primer that you are doing for us, Derek!  Short, to the point, not a lot of extra story-telling that I have to sift through.  Just the facts!

Love for the brevity, and now I love this series, also for the brevity.  Good work!

DotNetShoutout wrote Code Contracts Primer – Part 4: Utilizing Pre & Post Conditions - Derik Whittaker -
on 06-16-2009 10:21 AM

Thank you for submitting this cool story - Trackback from DotNetShoutout

About The CodeBetter.Com Blog Network
CodeBetter.Com FAQ

Our Mission

Advertisers should contact Brendan

Google Reader or Homepage Latest Items
Add to My Yahoo!
Subscribe with Bloglines
Subscribe in NewsGator Online
Subscribe with myFeedster
Add to My AOL
Furl Latest Items
Subscribe in Rojo

Member Projects
DimeCasts.Net - Derik Whittaker

Friends of
Red-Gate Tools For SQL and .NET


SmartInspect .NET Logging
NGEDIT: ViEmu and Codekana
NHibernate Profiler
Balsamiq Mockups
JetBrains - ReSharper
Web Sequence Diagrams
Ducksboard<-- NEW Friend!


Site Copyright © 2007 CodeBetter.Com
Content Copyright Individual Bloggers


Community Server (Commercial Edition)