How to tell code contracts a delegate specified as argument is Pure?

Question

Consider the following code:

int SomeField;
void Foo([Pure] Func<int, object> getData)
{
    Contract.Requires(getData != null);
    Contract.Requires(getData(this.SomeField) != null);
}

I get the following warning:

Detected call to method 'System.Func'2<System.Int32,System.Object>.Invoke(System.Int32)' without [Pure] in contracts of method '....Foo(System.Func'2<System.Int32,System.Object>)'

This warning makes perfect sense. But I'd still like to call the delegate in contracts and not get a warning (suppose I had warnings turned into errors). How do I achieve that?

I tried the attribute Pure, as shown in the example, but that doesn't work.

I'd also like to know why the PureAttribute can be specified on parameters. It wouldn't make sense if the type of the parameter wasn't a delegate type, and even if it is, it doesn't work as I'd expect, as I stated above.

Answer 1

The way to do this with the current Code Contracts library is to declare your own delegate type, like this:

[Pure]
public delegate U PureFunc<in T, out U>(T thing);

I think that the reason it doesn't work on delegate parameters is that it would be very hard to check in general :)

Answer 2

I'm not accustomed to the contracts framework, but from a purely logical way a delegate can't be pure, simply because it can take any method fulfilling the signature. There is no way you can guarentee that for all methods fitting that delegate, as it only requires one to break the contract.