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


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!

Comments below can no longer be edited.

21 Responses to Contract Annotations in ReSharper 7

  1. Avatar

    Roland says:

    August 15, 2012

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

  2. Avatar

    Michael Damatov says:

    August 15, 2012

    What for is the “forceFullStates” parameter?

  3. Avatar

    frank quednau says:

    August 16, 2012

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

  4. Avatar

    Martin says:

    August 16, 2012

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

  5. Avatar

    Joe White says:

    August 16, 2012

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

    Sergey Kuks says:

    August 17, 2012

    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.

    • Avatar

      Yosi says:

      May 27, 2014

      @Sergey Kuks
      You said “halt, void and nothing all means the same”
      I assume you meant to include “stop” in that list as well ?

  7. Avatar

    Lars-Erik Aabech says:

    August 20, 2012

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

  8. Avatar

    Jura Gorohovsky says:

    August 21, 2012

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

  9. Avatar

    repka says:

    August 31, 2012

    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: . 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. Avatar

    Sergey Kuks says:

    August 31, 2012

    @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. Avatar

    Jason Newell says:

    September 12, 2012

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

  12. Avatar

    Jura Gorohovsky says:

    September 12, 2012

    This comment explains why.

  13. Avatar

    Allon Guralnek says:

    October 22, 2012

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

  14. Avatar

    foo says:

    March 28, 2013

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

  15. Avatar

    Dmitri Nesteruk says:

    March 31, 2013

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

  16. Avatar

    Yosi says:

    May 27, 2014

    There’s no example for
    “param: canbenull”
    Could you clarify what that would mean ?

  17. Avatar

    Y says:

    August 28, 2015

    Is it possible to annotate methods containing out parameters? Something like this:
    bool TryGetValue(out TClass result)
    if return bool is true, then result out parameter is not null,
    if return bool is false, then result out parameter can be null?

    • Avatar

      Dmitri Nesteruk says:

      September 9, 2015

      Hi, yes indeed this is possible – the contract should be something like “=> true, result:notnull; => false, result:null” -- in other words, no information for the parameters (since there aren't any input ones), but giving the return value as well as the value of result.

      • Avatar

        Dave Cousineau says:

        September 19, 2018

        this doesn’t seem to work, but it’d be nice if it did

        • Avatar

          Dave Cousineau says:

          September 19, 2018

          k I figured out that you need to explicitly use reference types to get the warnings. a generic type that does not have a class constraint will not get the warning.

Discover more