Contract Annotations in ReSharper 7

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:

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!