Contract Annotations in ReSharper 7

Since the introduction of the Annotations feature of ReSharper, developers have had the possibility to get deeper control flow analysis by annotating their code with attributes such as [CanBeNull], [UsedImplicitly] and many others. With the release of ReSharper 7, the wide range of annotations is augmented with one very powerful type: contract annotations.

Brief Introduction to Contract Annotations

A contract annotation, as embodied by the ContractAnnotationAttribute, presents a completely new way of defining dependencies between method arguments and return values. This annotation is, in a way, a generalization of various existing annotations such as [TerminatesProgram] or [AssertionMethod], its primary goal being to let the developer specify precisely what return and output values a method may have given certain inputs.

Here’s an example — let’s say that we’ve got a method Adjust() that adjusts a Bitmap, but returns null if the argument is null:

Now, if we try to call this method with a null value and check against null, ReSharper will not complain because it doesn’t know that a null input yields a null output:

How can we help ReSharper? That’s right – we decorate the Adjust() method with a ContractAnnotation attribute, specifying that null inputs yield null outputs:

And lo and behold, the annotation lets ReSharper know that our usage has a redundant branch, leading to grayed-out code and the following inspection tooltip:

The extra annotation has allowed ReSharper to flag both the fact that the if condition is never satisfied and, therefore, the return statement is unreachable. Naturally, a context action is also offered to remove the unreachable code.

Contract Annotation Syntax

In order to define a method’s contract, we create a so-called function definition table. The table consists of several rows, each of which can define an input-to-output mapping in the form Input => Output or inverted in the form Output <= Input. For example, our definition of null => null from above could have equally been defined as null <= null.

Each Input is one or more (comma-separated) pairings in the form ParameterName: Value, with ParameterName being optional only in the case there is only one parameter. Value in this case can be one of true, false, null, notnull or canbenull. Here are some examples:

  • null => null omits the parameter name in cases there is only one parameter. Basically, null => null means that if the parameter has the value null, the method return value is also null. Note also that this annotation is automatically complemented with notnull => notnull.
  • foo:null => true states that if the parameter foo has the value of null, then the method returns true.
  • s:null=>false; =>true,result:notnull; =>false, result:null indicates that if the parameter s is null then the return value is false, otherwise the return value can either be true (in which case the value of the result output variable is not null) or false (in which case result is null).

In addition to taking a similar range of true/false/nullness values, the Output specification also allows the special values of halt|stop|void|nothing. These values all indicate that the method does not return normally. For example, an assertion method can be decorated with condition:false => halt.

Some Examples and Migration Advice

The following archetypical examples illustrate how one would apply contract annotations to certain well-known methods:

Of course, given the relative complexity of the contract annotation syntax, mistakes are unavoidable, but don’t worry: even here, ReSharper’s got your back. You see, not only does ReSharper use contract annotations, but it also provides inspections to make sure that you get the annotation just right. For example, if you try to specify a null annotation for a value type, ReSharper will catch that mistake for you:

If you’ve already been using annotations in ReSharper 6.x or ealier, several existing annotations have been made obsolete in ReSharper 7 to make way for the new contract attributes. The following table illustrates recommended changes:

Attribute Annotation
TerminatesProgramAttribute => void
AssertionMethodAttribute,
AssertionConditionAttribute
false => void

Please note: while the AssertionMethodAttribute has not been made obsolete, is is no longer used to indicate the fact that a particular condition halts the execution of the method. In other words, it is the AssertionConditionAttribute that has been made obsolete and needs to be replaced with a contract annotation.

Conclusion

Contract annotations represent a very powerful, flexible feature of ReSharper that lets developers add a layer of usage safety to their existing APIs. To start using them, simply go into ReSharper|Options, open the Code Annotations tab and copy the new implementation to your project. Good luck!

This entry was posted in ReSharper Tips&Tricks and tagged , . Bookmark the permalink.

15 Responses to Contract Annotations in ReSharper 7

  1. Roland says:

    YES !
    That’s exactly what I needed. Some of my methods could not be annotated before :) Cool

  2. Michael Damatov says:

    What for is the “forceFullStates” parameter?

  3. frank quednau says:

    Wouldn’t that be halt instead of void in both migration cases?

  4. Martin says:

    Does Resharper support contracts in Microsoft Code Contracts library format? That would be awesome.

  5. Joe White says:

    Cool feature.

    What is the difference between the four different “does not return normally” values (halt, stop, void, and nothing)? Halt and stop sound like the same thing, so it would be a pain if there was some subtle difference between the two that we needed to remember. Void would be a *normal* return for a void-returning method, so it makes no sense in your list of *abnormal* return codes. (Though it would certainly be abnormal for a non-void-returning method — that’d generate a stack imbalance!) And what does “nothing” do? It clearly doesn’t actually do nothing, because that wouldn’t be an abnormal return.

    Do you have anything that differentiates between “throws an exception” and “halts program execution immediately”? (I notice you don’t have a keyword for “throws”.) Or would that distinction not matter to your flow-control analysis?

    I agree with frank that both migration cases sound like they should be halt, not void.

    Also, how complete is ReSharper’s Intellisense for these expressions? If I mistype a parameter name, will ReSharper show an error? If I use a refactoring to rename a parameter, will it fix the expression? (Obviously it would rename it if I told it to look inside string literals, but it’d be great if it had deep enough integration that it could refactor it anyway, like it does with doc comments.)

  6. Sergey Kuks says:

    Here are some answers:
    halt, vois and nothing all means the same (and left for backward compatibility) and used to mark method that break control flow by throwing exception or terminating program. I.e. the
    [ContractAnnotattion("null => halt")]
    void AssertIsNotNull(object x) {
    if (x == null)
    throw new ArgumentNullException(“x”)
    }

    We did not manage to provide intellisense for the expressions yet, the only thing we did is error highlightings.

  7. Lars-Erik Aabech says:

    Ref @Martin. (+1)
    Microsoft Code Contract support would be awesome. :)

  8. @Martin, Lars-Erik
    Unfortunately support for Microsoft Code Contracts per se is not on the schedule for the reasons stated in this comment

  9. repka says:

    Awesome feature, one thing irked me though: what do you mean by null => null being “automatically complemented with notnull => notnull”? Is this a mistake? Why can’t notnull => null in some cases? How about true => false. Is it “automatically complemented” with false => true? I can understand such thing to be introduced for compatibility with some obsolete format of annotations, but if so, you should get rid of it as soon as possible, if you plan to keep these contracts for a while and extend them, stuff like that will cause trouble.

    Talking about extending them: please take a look at my proposal for Cleanup Annotations feature here: http://youtrack.jetbrains.com/issue/RSRP-329639 . It covers not only IDisposable tracking, but tracking of any values which must be somehow released, closed, completed, exited or cleaned up in any other way. E.g. files, sockets, transactions, identity impersonations, monitor locks, reader/writer locks, etc.

  10. Sergey Kuks says:

    @repka, If both null and not-null input may produce null output you probably better use CanBeNull annotation instead, because there is no obvious correlation between input and output.

  11. Jason Newell says:

    Really disappointed that Resharper has decided to invent their own form of code contracts rather than support the Microsoft version.

  12. Allon Guralnek says:

    What about “null => exception” Or is this the same as “null => halt”?

  13. foo says:

    I’ll repeat Michael’s question and ask, what’s the forceFullStates parameter for?

  14. Dmitri Nesteruk says:

    @Michael @foo setting forceFullStates=true causes R#’s analysis to become pessimistic, i.e., if the state of a variable is unknown, R# will assume that the variable might be null.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>