Introducing Advanced Code Contracts with the Entity Framework and Pex

With Code Contracts, Microsoft delivers its own flavor of Design by Contract for the .NET Framework. But wait, what is this thing sometimes called Contract-First Development? How will it change the way you develop software and write your unit tests? And first and foremost, how do you use Code Contracts efficiently? In this article, I will introduce Design

by Contract and Code Contracts, as well as give you a sneak preview of Pex-Microsoft’s new test-suite generator. Along the way, I will show you how to add contracts to ADO.NET entities and some interesting coding strategies, good practices, and pitfalls you may encounter while making a deal with your code.

A little bit more than a year ago, Microsoft deployed DevLabs (http://msdn.microsoft.com/devlabs), a new MSDN portal. DevLabs can be seen as a spinoff of Microsoft Research (http://research.microsoft.com), which is dedicated to, as its name implies, research in computer science. While the latter mostly targets academics, scientists, and research groups, the DevLabs audience is the developer community who lives and breathes Microsoft technologies.

You’ll find at DevLabs some of the research projects, like Code Contracts and Pex, which are most likely to end up as released products. From there, you can download trials and experiment with new .NET features before they are released, and have a word to say about what you try: the portal is as much about being a front-end for innovations as about collaboration and discussion. Active forums let you give your feedback directly to Microsoft, discuss things you like, argue about things you don’t, request cleaner features, and report bugs.

Note that I used Code Contracts version 1.2.20518.12 and Pex version 0.15.40714.1 for this article and that its content reflects the design, features, and state of these products as of July 2009. My code samples require the AdventureWorksLT2008 (http://www.codeplex.com/MSFTDBProdSamples) database; they are in C#, but be assured that Code Contracts work with any .NET language.

Now that you know where to get all these nice tools, let’s start talking about contracts and what they are meant for.

Introduction to Contracts

Whenever you create a class, interface, method, or property, you have a target goal in mind; a purpose that must be fulfilled by that specific piece of code. Sometimes, if you’re careless, you’ll just throw out the implementation and expect it to be used in a certain way, uncaring of what would happen if someone else tries to call it in an unexpectedly weird fashion. If you’re wiser, you may document it using XML comments and perform some sort of validation or provide unit tests to make sure your code behaves and is used as you expect it. In fact, at the very least, you most certainly always check your method arguments and validate your object states as shown in Listing 1, right?

While these ad-hoc validations may help alleviate your worries, wouldn’t it be better if you could just assume that you can code against your objects, knowing for certain that whenever you use them they answer to a predetermined set of rules? And that if for any reason they break those rules, there are safeguards preventing them from being handled in ways they shouldn’t?

These are feats that the formalism of Design by Contract helps you achieve.

Design by Contract

Design by Contract (DbC) is a software engineering methodology which states that collaboration between two elements of a system must be managed by a set of clauses, which form a contract. The parties involved in such a contract are referred to as the supplier and the client. As a service provider, the supplier agrees to deliver some benefits to the client and must ensure that they will be consistent with what the latter expects. On the other side, the client also agrees to abide by a certain set of obligations, or requirements, so that the supplier can answer its request.

To help enforce a contract, which is always specified by the supplier, Design by Contract defines three sets of clauses known as:

• Preconditions
• Postconditions
• Invariants

A precondition specifies the obligations of the client, which apply on a method or property to validate its arguments or the required object states for its execution. A postcondition defines the benefits the supplier delivers to the client, and also applies to a method or property to validate its return values or the expected resulting object states. An invariant is a clause that must hold true at all times, for the lifetime of an instance. Whenever one of these clauses is violated, Design by Contract prescribes that the execution of the code should automatically result in an error.

By analogy with the Listing 1 code sample, if a service offers to send a consumer’s orders by e-mail, the client of the service has an obligation to provide the service with a valid consumer instance (method precondition); the e-mail service itself must make sure it contains an initialized SMTP server name at all times (class invariant). The service contract may also require the availability of a network (method precondition). When all these conditions are met, the service supplier then ensures the order’s delivery, which is the benefit the client expects (method postcondition). If one of these clauses fails, an exception shall be thrown.

Because of the complexity involved in a software program, you cannot express all of its parts as a series of contracts. Going back to my example, expressing the success of an e-mail delivery as a postcondition could be difficult. This is why contracts are also sometimes referred to as partial software specifications.

Besides describing the contract clauses, Design by Contract provides rules for contract inheritance and guidelines for error handling. It also stipulates that you can use contracts for software documentation and testing. As such, it promotes Contract-First Development, which implies that the first thing you should do when you write a new code element is to write its contract’s clauses-I’ll come back to this statement later, when I talk about Pex.

I’ll show you now how Microsoft implemented these principles in DevLabs’s Code Contracts.

Code Contracts Basics

Since Code Contracts comes with an extensive user manual, which is also available as a separate download at DevLabs, I won’t cover every single feature it has to offer. Instead, I will highlight the basics required for this article and move on quickly to talk about how to strategically integrate contracts into an application, here using ADO.NET entities.

The Code Contracts project is an offshoot of Spec# (http://research.microsoft.com/en-us/projects/specsharp). Spec# is a C# extension language that supports contract constructs directly in the programming language. In contrast, you write Code Contracts statements using classes from the Code Contracts Library, which is language agnostic. While not entirely deprecated, Spec# is being moved to CodePlex as an open-source research project (http://specsharp.codeplex.com); how much and in which direction it will continue to evolve is unknown.

You will find the classes of the Code Contracts Library in the System.Diagnostics.Contracts namespace. These classes will be shipped directly within mscorlib.dll in .NET 4.0, but if you are using Visual Studio 2008 or targeting .NET 3.5, you’ll need to manually add a reference to the Microsoft.Contracts Library assembly in order to use them.

The main class of the Code Contracts Library is the Contract class. As you may expect, Contract offers methods to validate preconditions, postconditions, and invariants. It also extends that support to assertions and assumptions, which I will explain very shortly. All these methods are static and accept the result of a Boolean expression as input.

You specify preconditions using the Requires set of methods. They must be the first statements of a method body and can enforce validation of arguments, properties, fields, or object states:

Although postcondition statements validate the results of a method or other state upon method return, they must appear immediately after the preconditions. I will cover how they kick in at the end of a method execution when I talk about the Contract Rewriter and the Static Contract Verifier. You declare them using the Ensures method:

Note the call to Contract.Result<bool>(). This is how you refer to your method return value and how you use it in postcondition expressions. The code snippet simply states that it expects the return value of a method to be a bool whose value equals that of the HasErrors property.

The Requires and Ensures methods come with a few other special constructs; I encourage you to read the Code Contracts documentation to learn more about them.

Invariant statements are a bit different; you need to put them in a dedicated method and flag it with the ContractInvariantMethod attribute. The method name can be anything, but ObjectInvariant is the proposed standard for it:

In Design by Contract, invariants are meant to be true at all times. Currently, Code Contracts minimizes invariant evaluations so that they are taken into account only when you invoke a public method (that includes constructors) or a property setter. Otherwise, they are ignored. This is a feature you should be aware of if you choose to add invariants to your classes.

The Code Contracts Library also introduces support for assertions with the Assert method. You can use this method to validate a condition that should be true at a specific place in your code, for instance if you couldn’t or chose not to check it with the Requires or Ensures methods:

Alongside assertions come assumptions. They work like assertions, but you can declare them to help the Static Contract Verifier understand your code (more on this tool soon). The method to use is Assume:

At your option, when a contract clause fails, either an assertion occurs or a ContractException is thrown. ContractException gets generated in your assembly as private, and you must handle the more generic type Exception if you want to catch contract violations. Fortunately, you can customize the run-time contract error-handling behavior, as I will show later. Here is a sample exception message for a failed invariant:

Listing 2 presents a contract version of the common validations presented in Listing 1. Code Contracts also has support for using quantifiers over IEnumerable<> objects, for declaring inheritable contracts on interfaces and abstract classes, and for a few other features as well.

By: Martin Lapierre

Martin is an independent .NET Consultant living in Montreal, who is always interested in opportunities involving cutting-edge Microsoft technologies.

Martin has been doing n-tier software development and architecture on the Microsoft platform for more than 15 years and has experience in many business domains, such as microwave communications, manufacturing, engineering, finance, content management, laboratory informatics, text mining, code generation, and a few others.

When he's not doing .NET, you can find him trekking or kayaking in a national park, hitting balls on a tennis court, or adventuring in a faraway fantasy world.

martin_lapierre@devinstinct.com