Code contracts – suppressing warnings

The concept of designing by contracts (DbC) is a great one, and I think it should be obvious to most developers that adding pre- and post-conditions to methods can help ensure (even without unit tests) that the method is working well.

For my own projects I have always created a Check class that had a whole variety of methods for checking various conditions.  This has proved to be very useful, and although I don’t really love it when a pre-condition fails and crashes my program, it certainly makes it very easy to fix the problem right where it occurred rather than trying to hunt down the issue and figure out what unit test scenario I forgot (and therefore what new unit test needs to be written).

The new Microsoft Code Contracts that is being included with .NET 4 and VS2010 is really amazing, because it offers much more powerful post-condition checks and object invariants.  Without some very cool AOP tricks (and those only made possible with the next release of PostSharp) building an elegant object invariant method was very hard.AlexanderCoveredInDirt

Additionally, the idea of having a static contract verifier is absolutely amazing.  At compile time the verifier is able to tell me if I’m going to have problems at run-time, which means I don’t actually have to spend time running the unit tests or performing manual testing on my code.  That is, I know if I’ve got dirty code earlier in the development process than ever before.  Amazing.

Even more amazing is that the static checker sometimes makes suggestions as to what pre-conditions I should include!  So the static checker is really helping to make my code more robust.

The reason I’m mentioning all of this is becauase I’m currently writing a small demonstration application that I would like to be very complete.  Of course, I’m adding code contracts as a simple way of ensuring correctness (along with unit tests).  Unfortunately, the static verifier is giving me a whole bunch of warnings and a final message of:

CodeContracts: Checked 39 assertions: 29 correct 10 unknown

But the problem is that the “10 unknown” are reasonable complex and the static checker can’t figure it out, and each procudes two (very detailed which is great) warnings in the Visual Studio Error List.  For example, consider the following method on my document manager:

/// <summary>
/// Closes the given document and removes it from the document manager.
/// </summary>
/// <param name="document">The document to close</param>
public void Close(Document document) {
    Contract.Requires(document!=null, "The document to close must not be null");
    Contract.Ensures(this.ActiveDocument!=document, "After closing a document it cannot be the active document");
    Contract.Ensures(this.Documents.Contains(document)==false, "After closing a document it should not be part of the open documents collection");

    // Remove the document from the collection of open documents (which will raise the collection changed event)
    // If the document wasn't open (documents.Remove returns false) then there's nothing else to do here
    bool result = documents.Remove(document);
    if( result==false ) return;

    // If the document that was just closed was the active document then a new document must be made active
    if( document==this.ActiveDocument ) {
        // Determine which document will be made active now that we're closing the currently active document
        // This logic is simplistic but easy
        var newlyActiveDocument = this.Documents.Count==0 ? null : this.Documents[0];
        this.ActiveDocument = newlyActiveDocument;
    }//if - was active

    // Tell the document that it was closed
    document.DocumentClosed();
}

Any developer reading through the code would probably agree that a) the post-conditions are appropriate and, b) with the current implementation post-conditions will always be met.

Unfortunately, both of the post-conditions are very hard to check statically, and the static checker issues “unknown” warnings for both of them.  I definitely do not want a whole lot of warnings when building my application, especially warnings for un-provable post-conditions.  All these extra warnings can make it much harder to find the useful warnings that I actually want to fix.  So, how to eliminate the unnecessary “can’t check this” warnings?

CodeContractsManual Fortunately, the very excellent Code Contracts manual (installed with the Code Contracts VS plug-in) has a section on this: 6.5.4 Dealing with Warnings.  It has some very good suggestions and you should definitely read that section, but unfortunately nothing helps out here.

The next section (6.5.5) discusses how to build a “base line” file, which is basically an automatically created collection of all the current warnings.  This collection of warnings will be ignored in future compiles, allowing you to focus on new warnings.  However, to merge new warnings into this file must still be done by hand (although you could just delete the file entirely and then have the static-checker re-create it again with all the warnings).  I find that this approach is too coarse-grained to be easily effective, and it doesn’t work in a team setting when other developers might not have the base line file.  One solution would be to store the actual base line file in your SCM system, but that seems wrong.

Instead, section 6.5.6 has a very elegant and wonderfully fine-grained approach:  attribute the method with instructions to the static constraint checker that it shouldn’t emit this warning.  The special SuppressMessage attribute can even be applied to types, which is okay, and to assemblies.  Applying the attribute to assemblies however is no longer fine-grained and I don’t recommend it because it will hide any new warnings that you might want to know about (and might want to fix).

Dad feeding the birds I really like the approach when applied to just methods, because it means that a developer has specifically thought about this particular warning on this particular method and decided that it is okay to ignore it.   Unlike the broad strokes of the base-line file, this fine grained approach is clearly communicated to other developers and elegantly stored with the code in the SCM.

So our attributed method above now looks like this:

[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Contracts", "Ensures")]
public void Close(Document document) {
    Contract.Requires(document!=null, "The document to close must not be null");
    Contract.Ensures(this.ActiveDocument!=document, "After closing a document it cannot be the active document");
    Contract.Ensures(this.Documents.Contains(document)==false, "After closing a document it should not be part of the open documents collection");
...

And no more warning.

David Allen has a blog almost completely devoted to code contracts (and he’s the one that pointed me to this part of the manual!), so if you’re interested in reading more about this amazing technology you should definitely check out his blog: http://codecontracts.info/?blogsub=confirming#subscribe-blog

Robert

PS.  It’s now several hours later, and the static type checking just caught my first bug.  It warned me that a variable might be null and I hadn’t checked it.  It was correct, and I needed to modify my code to check if that variable was null and do something slightly different if it was.  Nice!  One more bug I don’t have to solve due to static contract validation.  🙂

Advertisements

8 comments so far

  1. David Allen on

    Your article has inspired me to try the static verifier again on some production code. In the past, I had only played with static verification on sample code. Seeing you use it in your demo project shows me it need not be difficult.

  2. robertmccarter on

    One problem I’ve found with this approach is that you can have provably FALSE contracts ignored – and the static checker will not tell you WHERE in your code the contract will certainly fail.

    Personally, I’d rather that if it’s “unknown” it is ignored, but if the contract is definitely going to fail then please tell me.

  3. David Allen on

    Yes, you have described the essential limitation of using static checkers that are currently available. Of course we would like to know if a contract is definitely going to fail. But real world static analysis tools are still very limited in what they are able to do. Given these limitations, static analysis tool developers have to strike a balance between false positives and false negatives.
    If they increase the sensitivity of the static checker to detect and report all of the contracts that are “definitely going to fail,” you will almost certainly be overwhelmed with false positives (lines of code that are not going to fail, but it reports them anyway because it is not very clever).
    If they decrease the sensitivity of the static checker in an effort to improve the signal-to-noise ratio, they will inevitably exclude some areas in the code that are at risk for failure.
    Since we are interested in this topic, we have the good fortune to have an article that just came out in the February 2010 edition of Communications Of the ACM. The full text of the article, “A Few Billion Lines of Code Later, Using Static Analysis to Find Bugs in the Real World”, is online at http://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext.
    I only read the article yesterday and I have been meaning to post a summary in my blog. But since they speak directly to the frustration you are describing, I wanted to refer you to the right away. The article is well written and fascinating to read.

    • robertmccarter on

      Very interesting article – and kind of scary the crazy things that some developers think, and other developers actually code.

      It sounds like a major benefit of including code contracts in applications today (even if they are littered with [SuppressMessage]) is that:
      1. It captures what the developer was expecting
      2. As the static verifier tool gets better the suppression of messags (especially for new code) will decrease. Ideally old message suppressions will even be revisited and removed.

  4. David Allen on

    I see it the same way. And since static checkers are still imperfect, we have the power of the runtime checking which is much more predictable. So if we are doing decent automated or manual testing, we will catch contract failures during the testing process and STILL eradicate them before the product is deployed to production. That is why I am still a big fan of automated testing, even though I love using contracts.

    • robertmccarter on

      Excellent point – suppressing warnings from the static checker does not in any way supress the checks at runtime, so they are still very useful.

  5. David Allen on

    Oh, and I keep meaning to tell you that the picture of AlexanderCoveredInDirt is adorable.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: