Contract Annotations in ReSharper 7August 15th, 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
[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
[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
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
How can we help ReSharper? That’s right – we decorate the
Adjust() method with a
ContractAnnotation attribute, specifying that
null inputs yield
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.
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
canbenull. Here are some examples:
null => nullomits the parameter name in cases there is only one parameter. Basically,
null => nullmeans 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 => truestates that if the parameter
foohas the value of
null, then the method returns
s:null=>false; =>true,result:notnull; =>false, result:nullindicates that if the parameter
nullthen the return value is
false, otherwise the return value can either be
true(in which case the value of the
resultoutput variable is not
false(in which case
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:
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!