Code Contracts in C# 4.0 – Part 1

Bugs occur. Once you accept that fact, you can do something about it. There are bugs in every piece of software with even a minimal level of complexity. Various options exist to address these. Manual testing is one, but it is often hard to reproduce, or just isn’t done. Automated testing is also possible, and useful, particularly with regards to test driven development. But even this has problems because poorly written tests require debugging themselves. In short, there is NO silver bullet. There are, however, more tools available.

Programming by Contract (the term “Design by Contract” is copyrighted by Bertrand Meyer) or Contract First development is a concept which asks developers to define formal specifications for interfacing to parts of software. It adds three important concepts to the developer lexicon, preconditions, postconditions and invariants. These three items are used to define “contracts” which define what the client of a component must do and what the component itself must do, in a formal manner. This is not the same as just adding a comment stating what must be true, it is a code based requirement that can stop execution dead in its tracks.

For all you hard core computer scientists out there, Programming by Contract has its roots in formal verification, as proposed by C.A.R. Hoare and others. The basic idea is that for any block of code, CodeBlock, a precondition should be defined that holds true before execution of the code block, and a postcondition must be defined which should hold true afterword. In text books, you will often see this written as:

{P}C{Q}

Where P and Q are assertions and C is the code block. To learn more about this, a good place to look is “The Science of Programming” by David Gries.

That’s enough of a computer science lesson for today. In .Net 4.0, Microsoft has added the concept of programming by contract. They originally did this as a language extended from C# called spec# but have since rolled a subset of this, the contracts library, into the .Net framework.

Normally when you mention contracts to .Net developers, they think of interfaces. While an interface is a contract, it doesn’t do much more than specify signatures of the individual methods. Code contracts let you declaratively state what must be true before, during and after execution of code. To use code contracts in .Net 4.0, you must first add a reference to System.Diagnostics.Contracts to your application. Also, to take full advantage of code contracts, you need to go to http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx#5 and download the standard or premium edition of the code contract tools based on the version of VS2010 you have. Without this, you will not be able to check contracts at runtime. Once you’ve downloaded it, install it and we can get started.

In C#, there are four things which can be used to build a code contract:

Preconditions – Checked at the start of a methodPostconditions – Validated before a method exitsInvariants – Verified after a public method is called within a class.Assertions – Verified anywhere they occur

To get started, we will write a simple method on an Order object, GetTotal. This method will operate on an order with a list of items, and return the total price of the order. So first, we should establish what we expect to hold true BEFORE we execute our method (which we will call GetTotal) and what we expect to be true when we receive our results.

Preconditions

The order must not be nullThe list of items within the order must not be nullEach price must be non-zero

Postconditions

The total must be non-negative and greater than 0The total should be the sum of all the items within the order (this is also the result…)

Obviously this list is simplistic. Many more preconditions can be established. We will use the following code for this example:

public class Order { private List _orderItems = new List(); public Order(IEnumerable items) { _orderItems.AddRange(items); } public void AddItem(OrderItem item) { _orderItems.Add(item); } public List GetItems() { return _orderItems; } public double GetTotal() { double total = 0.0; if (_orderItems != null && _orderItems.Count > 0) { foreach (OrderItem item in _orderItems) { total += item.Price; } } return total; } } public class OrderItem { public string Name { get; set; } public double Price { get; set; } }

So given the above code, we are going to see how code contracts can help us ensure that our code does precisely what is expected of it.

Something you need to be aware of is that unless you define the symbol CONTRACTS_FULL most of your contract code will be stripped out during compilation, as often, it is not something that is desired in production code. If you enable contract checking in the project properties’ Contract tab, this symbol will be defined (You must have installed the contract package we downloaded earlier). However, due to some weird interactions with other software (Resharper particularly) it is not a bad idea to add this to your csproj in the DefineConstants section. Also, to see the results, I would check “Assert on contract failure” in the project properties.

To enable the contracts to be enforced at run time, you must first run the binary rewriter. The binary rewriter arranges the code appropriately and inserts calls to it in the actual application. It also replaces compile time instances of the contract with runtime ones that actually execute when the code is executing. If you don’t run the rewriter, you will get tons of runtime errors. The rewriter is called ccrewriter.exe and is called automatically when you check contract checking in the properties tab.

Before we get to the actual code, there is one thing we must examine first. The purity of your code. Now I am sure, every developer thinks his or her code is as pure as the first new snow. But what we are talking about is whether or not your code has side effects. Basically when you call any of the contract verification methods provided by Microsoft, the code you are referencing in those calls must not cause or call any code that causes side effects. In essence, the method cannot make any visible state changes. For example, no updating class level variables. Your data is passed in and out in a purely functional manner. For example, a function like IsEmailValid(string email) can be marked pure if it doesn’t modify the state of the parameter email. To indicate that a method is pure, mark it with the [Pure] attribute. Note that we are NOT saying that your method itself must be pure; just any calls to the contract library requiring a function call must be pure.

There are three methods used to define preconditions in .Net 4.0. These are Contract.Requires, Contract.Requires and Contract.EndContractBlock. These should be established at the start of a method. Also note that preconditions are inherited and there is no way for a subclass to prevent the parent from ensuring them. Similarly, when preconditions are defined on interface members, (explained later) they will be integrated with the concrete classes as well. This is much more complete than an assert statement which just acts on the code it currently is executing on. Also, there are tools that can generate documentation from your preconditions.

Keep in mind that contracts are not exceptions. Don’t use them to make decisions impacting the flow of your program. Instead, they are primarily used to catch bugs (as opposed to catching exceptions). Contracts are a programmer level tool, not necessarily an end user one. Catch bugs in client calls. Catch exceptions with good old exception handling. Also, don’t create preconditions on things the client can’t see. If you don’t expose it, the client cannot ensure it.

So finally, let’s create some code which uses preconditions:

public double GetTotal() { double total = 0.0; if (_orderItems != null && _orderItems.Count > 0) { foreach (OrderItem item in _orderItems) { total += item.Price; } } return total; }

As stated above, we want to ensure the following preconditions:

The order must not be nullThe list of items within the order must not be nullEach price must be non-zero

In code, this would look like:

Contract.Requires(GetItems().Count > 0); // Assertion for #2. GetItems must be pure

Contract.Requires(GetItems().TrueForAll(item=>item.Price >0)); // #3

No assertion is needed for the first condition because it will always be true (otherwise this code would never get executed). So the following code changes are necessary:

GetItems must be attributed as pure [Pure] public List GetItems() { return _orderItems; }

2. GetTotal should be modified as follows:

public double GetTotal() { // Establish preconditions Contract.Requires(GetItems().Count > 0); // Assertion for #2. GetItems must be pure Contract.Requires(GetItems ().TrueForAll(item=>item.Price >0)); // #3 double total = 0.0; if (_orderItems != null && _orderItems.Count > 0) { foreach (OrderItem item in _orderItems) { total += item.Price; } } return total; }

In this installment we defined what preconditions, postconditions, invariants and contracts are. We also took a look at some simple preconditions. In the next installment, we’ll look into postconditions and start examining other features of the contracts library.

Written by Larry Schoeneman.

Larry Schoeneman is a software developer with over 20 years of experience, focused on Microsoft products and technologies as well as utilizing agile methodologies to build better software.

If you found this post useful you may also want to check these out:

Develop Rock-Solid Code In PHP: Lay The Foundation, Part 1Develop Rock-Solid Code In PHP: Use Variables Effectively, Part 2Debugging PHP code using debug_backtraceCode reuse in PHP frameworksColor Code ConverterSnipplr: A Code Repository for Designers and Developers

View the original article here