Published: 02 Oct 2009
By: Dino Esposito

In a previous DotNetSlackers article I explored preconditions. In this article, I'll focus on another aspects of Code Contracts - postconditions. Before going any further, though, let me briefly summarize some of the design choices the team made to expose the Code Contracts API.

Contents [hide]

The Code Contracts Series

  • Code Contracts Preview: Preconditions  In this article, Dino Esposito reviews code contracts in .NET using sample Visual Studio 2008 applications.
  • Code Contracts Preview: PostConditions In this article, I'll focus on another aspects of Code Contracts - postconditions. Before going any further, though, let me briefly summarize some of the design choices the team made to expose the Code Contracts API.
  • Code Contracts Preview: Invariants In this article, I'll go through the concept and implementation of class invariants as supported by the .NET Framework 4 Code Contracts API.
  • Introduction

    The Code Contracts feature you will find in the .NET Framework 4.0 is the newest Microsoft's implementation of an old and effective idea that came up two decades ago implemented in the Eiffel programming language. Originally named Design by Contract, it refers to a set of language constructs that express preconditions, postconditions, and invariants to be fulfilled in class methods.

    When you look at Code Contracts in the .NET Framework 4, you see that it is not coming out as tightly integrated with other language constructs. In other words, the current implementation takes the form of a library that extends the Base Class Library (BCL) rather than that of a set of new language keywords.

    In a previous DotNetSlackers article I explored preconditions. In this article, I'll focus on another aspects of Code Contracts - postconditions. Before going any further, though, let me briefly summarize some of the design choices the team made to expose the Code Contracts API.

    Library vs. Language

    The .NET platform can be programmed using a variety of languages, all of which share the whole set of features in the BCL. You can call any of the classes in the BCL from any of the managed languages - and always in the same way. Code Contracts just work this way. You don't need a different set of keywords to set, say, a precondition in Visual Basic .NET and in C#.

    The first analogy that comes to mind is with LINQ. Both LINQ and Code Contracts are, at the very end of the day, a .NET idiom. In particular, LINQ is the .NET idiom for the Query Object pattern. Code Contracts is the .NET idiom for the DesignByContract pattern.

    LINQ is implemented as a BCL extension and makes its services available to any code that runs within the CLR. For this reason, LINQ functionalities can be used at no additional charge in C#, Visual Basic .NET, and any other managed language. However, when you write a LINQ query, you may choose between classic procedural code where you employ static methods on IQueryable objects and a sort of simplified and sweeter syntax based on a new set of language specific keywords such as from, in, where, and select.

    The preceding code is functionally equivalent to the following:

    LINQ language keywords are plain syntactic sugar specific of just one language and the language compiler takes care of translating them into calls to the BCL classes and methods. As of today, no such of syntactic sugar is available for code contracts.

    All in all, the decision of implementing Code Contracts at the BCL level is right as it enables a feature for all of the languages using the .NET Framework, and not just one of them. At the same time, a bit of sugar would make the whole thing easier to digest and may even decouple the developer's API from the internal implementation.

    In order to use Code Contracts in a .NET Framework 4 application, you don't need to link any additional external assemblies. All you do is adding a reference to a new namespace in the class files where you need it:

    The infrastructure for code contracts is implemented in the system.core assembly.

    Making Sense of Postconditions

    In general, using design-by-contract is a sort of all-or-nothing approach. If you choose it, then you are going to have at least preconditions and postconditions all over the place. If you correctly implement preconditions in your methods then you determine a precise situation: your method can't throw if not for exceptional events.

    Put another way, with preconditions in place no method can fail because of it received invalid or unacceptable input. Can a method throw because it gets an exception from an externally referenced object? Look at this code:

    Can the OrderHelper class throw an exception? Sure, it can. However, you use design-by-contract in a testing scenario. And testing should always take place on isolated components. In a perfect world, you would inject OrderHelper logic into the AddOrder method and provide a fake OrderHelper in tests. A fake OrderHelper will just work and won't throw.

    From this, it results that in an ideal design-by-contract scenario exceptions are:

    • Those thrown by preconditions;
    • Those caused by exceptional events that you don't control directly such as I/O or network failures, stack overflow, or perhaps out-of-memory exceptions;

    However, in a less-than ideal scenario (much more common in this real world…), a method may have a tight dependency on other components that are not tested in isolation, as OrderHelper in the preceding code snippet. You won't have a way to replace a fake object and under test those external objects may throw an exception that bubbles all the way up the stack until it reaches the caller.

    If you live in a less-than ideal scenario, then the category of "exceptional events" must be enlarged to include also exceptions generated by dependencies.

    So what are postconditions, anyway? They are checks about normal and exceptional returns. A normal return check identifies an expected condition of the object that must be observable at the end of the execution. An exceptional return check identifies conditions on the object that must be observable in case of an exception thrown by a dependent object, or originated from an exceptional event.

    Does it make sense to check conditions on exceptions? Yes, it is a form of defensive programming aimed at ensuring that some firm points regarding the state of the object are ensured also in case of code failure. However, such postconditions should be as specific as possible. The reason is that postconditions are not runtime code aimed at showing a nice UI in case of troubles. Postconditions are rather helping you to test that the object is a given state after a particular exceptional event. An exceptional return check allows you to make a verifiable statement about the state of the object if, say, the system runs out of memory or fails accessing the network, during the execution of the method. Not just any Exception type, but very specific exceptions.

    Postconditions in Action

    The primary Contract method you use for postconditions is Ensures. The method comes in various forms, as below:

    It basically takes a Boolean expression, plus an optional message, and checks that the condition is verified when the method that contains it reaches its natural end. Another method exists to ensure a given condition holds under abnormal termination of the method. This method is EnsuresOnThrow.

    You can place calls to Ensures and EnsuresOnThrow anywhere in the body of the method. Have a look at what is shown in Figure 1.

    Figure 1: A disassembly view of the sample application.

    A disassembly view of the sample application.

    In the sample class Customer, the setter method of the ID property is defined with the following code:

    As you can easily imagine, the Ensures call makes not much sense and I placed it there only to test the postcondition. The figure shows a disassembly view of the setter as it is being actually executed. Regardless of where you place a postcondition in your source code, it is being moved automatically at the end of the method - where it logically belongs.

    Overall, you can use the elements of the Code Contract API to build a sort of a declaration of your intent. You place preconditions and postconditions together at the beginning of the method to specify the "contract" exposed by the method. It is the compiler - more precisely, a new tool called the rewriter - that recognizes the specific API and reshapes it to a more natural order. Contracts are essentially declarative but are coded as methods instead of attributes because of the much greater expressivity that methods allow over attributes.

    PostConditions vs Assert

    When you think of preconditions, you immediately envision a way to have them in place without using a specific new API. An if-then-throw statement, in fact, indicates exactly the type of code the compiler will emit for a precondition. What's the quick replacement for a postcondition? A plain Assert can make the trick, but not as richly as the Contracts API.

    Assert is good at checking conditions on normal returns, but not for exceptions. In addition, the Contracts API offers other helper methods such as those listed below:

    Method Result<T> indicates the return value of the method, if any. Of course, you will get a compile error if you try to use the method in a void method. Method OldValue<T> receives the name of a method's variable and returns the value of the variable at the beginning of the method. Finally, ValueAtReturn<T> is used to reference the value of an output parameter in a postcondition. In theory, you could just build a postcondition that uses the plain variable name without resorting to an ad hoc method, as shown below.

    If you do so, though, some compilers - specifically, the C# compiler - complains about the use of unassigned variables. Using ValueAtReturn<T> solves the issue.


    The bottom line is that Code Contracts can be simulated, for some aspects, with plain code. A postcondition is in this regard similar to using a plain Assert. However, the Code Contracts API is functionally richer and, even more importantly, represents a common API for tools (i.e., static checkers) to work with. The API is young, but will grow. For sure.

    <<  Previous Article Continue reading and see our next or previous articles Next Article >>

    About Dino Esposito

    Dino Esposito is one of the world's authorities on Web technology and software architecture. Dino published an array of books, most of which are considered state-of-the-art in their respective areas. His most recent books are “Microsoft ® .NET: Architecting Applications for the Enterprise” and “...

    This author has published 54 articles on DotNetSlackers. View other articles or the complete profile here.

    Other articles in this category

    Android for .NET Developers - Location and Maps
    In Windows Phone and iOS getting the current position of the device in terms of latitude and longitu...
    Android for .NET Developers - Using Web Views
    In this article, I'll show a native app that contains a web-based view. The great news is that HTML ...
    Android for .NET Developers - Building a Twitter Client
    In this article, I'll discuss the features and capabilities required by an Android application to ta...
    Developing a Hello World Java Application and Deploying it in Windows Azure - Part II
    In this article we will see the steps involved in deploying the WAR created in the first part of thi...
    Ref and Out (The Inside Story)
    Knowing the power of ref and out, a developer will certainly make full use of this feature of parame...

    You might also be interested in the following related blog posts

    Foxit PDF Previewer update read more
    Winforms Release History : Q2 2009 SP1 (version 2009.2.9.729) read more
    Thoughts on the Code Contracts Preview for .NET 4.0 read more
    ASP.NET MVC Source Refresh Preview read more
    Updated to MS Ajax RC read more

    Please login to rate or to leave a comment.