Contract annotations

Contract annotations let you define expected outputs for given inputs, or put in other words, define dependencies between reference type and boolean arguments of a function and its return value. The mechanism of contract annotations allows creating APIs that could be consumed in easier and safer way.

You can implement contract annotations by decorating your functions with the [ContractAnnotationAttribute]. If you want to do it in your source code, reference the JetBrains.Annotations namespace. You can also annotate functions in existing binary modules using external annotations.

How it works

To quickly understand how and why you could use contract annotations, look at the example below.

In this example, we decorated the function Adjust with the contract annotation attribute. The attribute argument in this case means, that a null argument always yields a null return. You can easily read the code of this example to see that the function works this way, but in real-life code this dependency might not be that obvious. Anyway, the main thing here is the contract annotation attribute that describes how the function handles the input value.

When we call the Adjust function with a 'null' argument, ReSharper finds and highlights a bunch of issues at once. First of all, it highlights the function call with a null argument, warning that this expression is always null. Then, it keeps tracking the adjusted variable that was initialized with this expression, and now is also 'null'. When we check the adjusted variable for inequality to 'null', ReSharper warns us again that this comparison is always false. Finally, ReSharper greys out code in the 'if' statement as unreachable:

ReSharper's code inspection based on contract annotation

Syntax of contract annotations

Use the following syntax to specify input-output dependencies for contract annotations:

[ContractAnnotation("[paramName:][input] =>
            output [; [paramName:][input] => output]", [forceFullStates:true])]

The input can be:

null/notnull for reference type parameters
true/false for boolean parameters.

The output can be

null/notnull/canbenull for the return value of reference type
true/false for the return value of boolean type
halt|stop|void|nothing (which are interchangeable) to indicate that the function does not return normally. That is, it throws an exception or halts program execution.

The optional boolean forceFullStates parameter, which is false by default, allows you force the pessimistic mode for the nullability analysis. That is if the method return value is not defined by the contract condition, ReSharper will assume that it might be null.

Remarks:

You can omit paramName if there is only one parameter (see the example above)
You can omit both paramName and input if there are no parameters:
[ContractAnnotation("=> halt")] public void TerminationMethod()
or if the function has the same output independently on the input:
[ContractAnnotation("=> halt")] public void TerminationMethod(object data, bool flag)
You can add several conditions for the same parameter:
[ContractAnnotation("input:null => null; input:notnull=>notnull")] public object Transform(object input, bool flag)
You can reverse conditions, that is input => output is equal to output <= input:
[ContractAnnotation("null <= surname:null")] public string GetName(string surname)
You can also specify expected values for 'out' parameters. If you want to specify both a return value and an 'out' parameter for the same input condition, use the comma:
[ContractAnnotation("s:null => false,result:null")] public bool TryParse(string s, out object result)

Validation of contract conditions

If you decorate functions with contract annotation in the source code, ReSharper verifies contract conditions according to the function signature. If the contract annotation does not suit function parameters, ReSharper displays a warning:

The same happens if the contract annotation does not suit the return value.

Last modified: 21 July 2022