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 => nullomits the parameter name in cases there is only one parameter. Basically,null => nullmeans that if the parameter has the valuenull, the method return value is alsonull. Note also that this annotation is automatically complemented withnotnull => notnull.foo:null => truestates that if the parameterfoohas the value ofnull, then the method returnstrue.s:null=>false; =>true,result:notnull; =>false, result:nullindicates that if the parametersisnullthen the return value isfalse, otherwise the return value can either betrue(in which case the value of theresultoutput variable is notnull) orfalse(in which caseresultisnull).
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!
YES !
Cool
That’s exactly what I needed. Some of my methods could not be annotated before
What for is the “forceFullStates” parameter?
Wouldn’t that be halt instead of void in both migration cases?
Does Resharper support contracts in Microsoft Code Contracts library format? That would be awesome.
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.)
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.
@Sergey Kuks
You said “halt, void and nothing all means the same”
I assume you meant to include “stop” in that list as well ?
Ref @Martin. (+1)
Microsoft Code Contract support would be awesome.
@Martin, Lars-Erik
Unfortunately support for Microsoft Code Contracts per se is not on the schedule for the reasons stated in this comment
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.
@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.
Really disappointed that Resharper has decided to invent their own form of code contracts rather than support the Microsoft version.
@Jason
This comment explains why.
What about “null => exception” Or is this the same as “null => halt”?
I’ll repeat Michael’s question and ask, what’s the forceFullStates parameter for?
@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.
There’s no example for
“param: canbenull”
Could you clarify what that would mean ?
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?
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 ofresult.