Is there a common PureAttribute that ReSharper and Code Contracts can both use?

Question

I'm writing in C# with ReSharper 8.0 and VS2012 for .NET 4.0.

ReSharper includes an attribute: JetBrains.Annotations.PureAttribute. This is used to provide the inspection "Return value of Pure method is not used".

Code Contracts includes an attribute: System.Diagnostics.Contracts.PureAttribute. This is used by the code contract checking to ensure that the call will produce no visible state changes, and therefore will not require re-checking the object's state.

Currently, to get the functionality of both of these tools, methods need to be annotated with attribute from each. Worse, because they both share the same type name, you need to qualify each attribute.

[Pure]
[Jetbrains.Annotations.Pure]
public bool isFinished() {
    ...

To avoid this situation, there should be three approaches:

1. write a placeholder recognized by both ReSharper and Contracts
2. get ReSharper to recognize the Contracts attribute
3. get Contracts to recognize the ReSharper attribute

Are any of these possible?

Answer 1

ReSharper already understands System.Diagnostics.Contracts.PureAttribute and treats it the same way as JetBrains.Annotations.PureAttribute, so you can just use the one from Code Contracts, and both tools will be happy.

Answer 2

Approach 3 offers the solution: Jetbrains.Annotations.PureAttribute IS recognized by Contracts.

However, you still will encounter the name conflict problem when using Contracts and PureAttribute in your code. This can be shorthanded with a using statement:using RPure = Jetbrains.Annotation.PureAttribute;

Here's some code that demonstrates the attribute successfully working for Contracts and ReSharper.

public class StatefulExample {

    public int value { get; private set; }

    public StatefulExample() { value = 1; }

    //Example method that would need to be annotated
    [Jetbrains.Annotations.PureAttribute]
    public int negativeValue() { return -value; }

    public static void useSpecificState(StatefulExample test) {
        Contract.Requires(test.value == 1);
    }

    // ---

    public static void pureMethodRequirementDemonstration() {
        StatefulExample initialState = new StatefulExample();
        useSpecificState(initialState);

        StatefulExample possiblyChangedState = new StatefulExample();
        //"Return value of Pure method is not used" here if annotated.
        possiblyChangedState.negativeValue();

        // "Requires unproven: test.value == 1" if NOT annotated.
        useSpecificState(possiblyChangedState);
    }

}