Published: 11 Nov 2009
By: Dino Esposito

In this article, I’ll go through the features of side contract-based tools in .NET Framework Code Contracts. In particular, I’ll focus on Assert and Assume methods.

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.
  • Code Contracts Preview: Assert & Assume In this article, I’ll go through the features of side contract-based tools in .NET Framework Code Contracts. In particular, I’ll focus on Assert and Assume methods.
  • Introduction

    Software contracts are often identified with preconditions, postconditions and invariants. And these are indeed the most valuable pieces of the API by far. However, in the .NET Framework 4.0 implementation of software contracts you find other elements that altogether provide for additional services, extra tools, and in the end more programming power. These elements drive the behavior of both the run time code and static checker tools that attempt to verify contracts statically without running the code.

    In this article, I'll go through the features of side contract-based tools in .NET Framework Code Contracts. In particular, I'll focus on Assert and Assume methods.

    The Contract.Assert Method

    Assertions are a basic element of any debug and test scenario in the widest possible scope. With Code Contracts, you are not debugging or testing your code, but you are just trying to write it in a way that saves you debugging sessions and makes tests pass quickly and seamlessly.

    In .NET, assertions come in the form of the Debug.Assert method which basically checks for a condition. Next, if the condition is true, nothing happens. Instead, if the condition is false the Debug.Assert method sends a failure message to the collection of registered listeners and the application breaks in debug mode. If the application runs with a user interface, then you get a message box that also shows the call stack and buttons for you to decide about the next action to take.

    The Debug.Assert method is defined in the System.Diagnostics namespace and is mostly used to identify logic errors at development time. It only works in debug builds; to detect failed assertions left in the code at run time you have to switch to Trace.Assert instead.

    It is recommended that the Boolean condition you specify as an argument to the Debug.Assert function involves exclusively variables and any call to methods is avoided. This could, in fact, result in nasty side effects when you later switch to release mode.

    This aspect of coding is known as purity of methods; it is nothing new but it is an aspect that gets a particular emphasis in Code Contracts documentation. A pure method is a method with a behavior that doesn't update any pre-existing state. In other words, a pure method is not allowed to modify any objects that have been created before the method was invoked. A pure method is either read-only or only updates its own temporary variables.

    As far as the Code Contracts API is concerned, pure methods are methods explicitly marked with the [Pure] attribute, property getters, operators, and any static methods on Contract, String, Path or Type objects. Finally, the Code Contracts API also considers pure any invoked delegate, as long as the delegate type itself is decorated with the [Pure] attribute.

    Even though the section refers to Contract.Assert, I mostly talked about Debug.Assert thus far. So in which way are the two different and equally useful to developers?

    As far as the run time behavior is concerned, there's really no difference between Contract.Assert and Debug.Assert. You can definitely use Contract.Assert in any place where you can use Debug.Assert. The syntax is also identical and the same considerations apply as for the purity of invoked methods.

    What's the real purpose of having a specific Assert method in the Code Contracts API?

    The Code Contracts ecosystem contains a programming API as well as a bunch of executable that process contracts in various ways. So, for example, the rewriter tool ensures that the final IL code contains proper calls to contract methods executed from the right places. The static checker tool, instead, examines your code without executing it and tries to prove that all of the contracts are satisfied. The static checker tool requires Visual Studio Team System and lists unproven contracts to fix saving you from going through all of your code in a debug session to see if the contract is verified or covering it with unit tests. The checker tool, however, has to be seen as a quick way to spot contract violations; it works along with debugging and testing; it doesn't replace any of them.

    Essentially, in the context of Code Contracts assertions need to have a dual interface - towards runtime execution and towards static checks. That's the reason why a new API is required that seems to be just a clone of Debug.Assert from a run time perspective. The static checker tool will attempt to prove any Contract.Assert it finds along the way and it will emit a warning if it fails.

    In the end, you use Contract.Assert in the same way and in the same places where you would use Debug.Assert. The benefit you get out of it is that your code will be able to be statically checked. If you don't plan to use static checking, then you can blissfully ignore Contract.Assert and keep on using Debug.Assert for any assertions you may need to insert in the code.

    The Contract.Assume Method

    The method Contract.Assume exists to let you specify an assumption about your code. An assumption is a condition that has to be assumed to hold at a given point of execution. It goes without saying that if you're running the code than assumptions simply do not make sense: either your code works as expected or not. You can catch any of these facts by using an assertion. An assertion asks the system to ascertain whether the specified condition is true; an assumption tells the system that a given fact has to be considered true from now on.

    The natural habitat for assumptions is in the context of the static checker tool. The Contract.Assume method takes a Boolean expression as its argument (plus an optional string message) and instructs the static checker tool.

    The static checker will consider any assumptions it receives through the method as definitely true and add them it to its own collection of facts about the application being checked. The static checker tool has an obviously limited set of capabilities compared to running an instance of the application. It may not be able to verify assertions because it may lack valuable information resulting from execution of some code. Assumptions help the checker to grab a more precise picture of the application's scenario and sync its collection of facts with the real runtime state of the application.

    How can the checker know about the results of an executed method without actually running it? If you use Code Contracts all the way through then you happen to have postconditions on any methods. Hence, postconditions may inform the checker about the characteristics of the value being returned by the method. The method shown below uses the Ensures postcondition to inform that it is expected to return a value greater than zero.

    Now let's consider the caller of CalculateSomeValues and how the checker can go about it.

    The assertion is always honored at run time. The static checker, though, will let it pass only if you have specific postconditions in the method being called. If you remove the Ensures call in CalculateSomeValues then the following assertion can't be proven by the checker and results in a warning.

    It would be preferable to leave the Ensures in place but what, say, if you don't control that piece of code and need to go without valid postconditions? In that case, Contract.Assume would help.

    When it reaches the Contract.Assume line, the checker adds the specified condition to its facts; it doesn't emit any warning, and can proceed further to prove next assertions and preconditions.

    Finally, note that assumptions are conditionally defined. This means that they exist in the build only when the full-contract symbol or the DEBUG symbol is defined. At run time, using the Contract.Assume method is equivalent to using the Contract.Assert method.

    Assumptions and Design

    Should you use assumptions or assertions in Code Contracts? As mentioned, assumptions make only sense if you're doing static checks. If not, you can just forget about them.

    In general, it may be preferable, and kind of safer for the effectiveness of design, if you start writing code using only assertions. As you make progress, and run the checker, you may see that too many assertions are unaccountably failing during static analysis.

    If that is something you can fix with postconditions - that is, giving each method its own full code contract - you do so. Otherwise, you may opt for assumptions if you figure out that given the structure of the code the checker can't just figure it out entirely all by itself.

    Summary

    Assertions are a fundamental piece of code. They help in debug and in testing. Assertions, however, do require that code executes. The static checker, instead, is a tool for static analysis of code. The checker will read the code and attempt to prove it right. (Yes, more or less what we were doing 20 years ago or so while reading BASIC and Clipper printed listings to catch bugs.)

    Assertions work, but not always for a checker. The checker may sometimes lack the information it needs to honor the assertion. This is where assumptions fit in. Assumptions are, in a way, the extreme ratio. They should be used when you cannot apply entirely core contract stuff such as postconditions as well as in some corner cases that may always show up.

    <<  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


    Winforms Release History : Q2 2009 SP1 (version 2009.2.9.729) read more
    HTML Stripping Challenge read more
    Using Assert.AreSame read more
    Improving MoQ to allow arrange-act-assert testing style read more
    MoQ now uses xUnit for its unit tests read more
    Generic constraint for Rhino Mocks - make unit tests more readable read more
    Reference assemblies the clean way in F#, not the ugly way read more
    Test Secure Class Instantiation Helper Method read more
    XUnit.NET aims to be the Next NUnit, but it's too soon read more
    Productive Unit Testing with Specialized Assertion Classes in MbUnit read more
    Top
     
     
     

    Discussion


    Subject Author Date
    placeholder What is difference between Assert and Requires? Ashish Mundra 12/25/2010 3:06 AM

    Please login to rate or to leave a comment.