Contract Annotations in ReSharper 7

Posted on August 15, 2012 by Dmitri Nesteruk

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!

#ReSharper #ReSharper 7

Comments below can no longer be edited.

21 Responses to Contract Annotations in ReSharper 7

Roland says:
August 15, 2012
YES !
That’s exactly what I needed. Some of my methods could not be annotated before 🙂 Cool
Michael Damatov says:
August 15, 2012
What for is the “forceFullStates” parameter?
frank quednau says:
August 16, 2012
Wouldn’t that be halt instead of void in both migration cases?
Martin says:
August 16, 2012
Does Resharper support contracts in Microsoft Code Contracts library format? That would be awesome.
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.)
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.
- 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 ?
Lars-Erik Aabech says:
August 20, 2012
Ref @Martin. (+1)
Microsoft Code Contract support would be awesome. 🙂
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
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: 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.
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.
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.
Jura Gorohovsky says:
September 12, 2012
@Jason
This comment explains why.
Allon Guralnek says:
October 22, 2012
What about “null => exception” Or is this the same as “null => halt”?
foo says:
March 28, 2013
I’ll repeat Michael’s question and ask, what’s the forceFullStates parameter for?
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.
Yosi says:
May 27, 2014
There’s no example for
“param: canbenull”
Could you clarify what that would mean ?
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?
- 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.
  - Dave Cousineau says:
    September 19, 2018
    this doesn’t seem to work, but it’d be nice if it did
    - 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.

Contract Annotations in ReSharper 7