How to use code contracts when deriving from interfaces like IDictionary<T, U>?

Question

One class I am writing implements IDictionary<string, object>. In my CopyTo implementation, I would like to use code contracts: stuff like Contract.Requires<ArgumentNullException>(array != null).

But, I get this warning (with some namespaces removed for readability):

Method 'LuaDictionary.CopyTo(KeyValuePair<String,Object>[],Int32)' implements interface method 'ICollection<KeyValuePair<String,Object>>.CopyTo(KeyValuePair<String,Object>[],Int32)', thus cannot add Requires.

I see that there are some related questions, but they all seem to have to do with interfaces that are under the user's control. Obviously, IDictionary<T, U> is not under my control, so I can't annotate it with ContractClassFor or anything like that.

So am I just unable to use code contracts here? If so... major bummer...

Answer 1

It is a bummer, but is understandable because client code that uses instances of your class as IDictionary<string, object> should not have to meet preconditions that are not expected of IDictionary<string, object>.

You can read the answer provided to this SO question, which links to and quotes the Code Contracts User Manual, and you can look at this article, which explains the situation this way, and goes on to provide a simple example:

Note that the Liskov's substitution principle holds true for Code Contracts in much the same way it holds for plain classes. The Liskov's principles says the following:

Subclasses should always be substitutable for their base classes.

In terms of the Code Contracts API this means that a derived class (or a class that implements a contract-based interface) should not expect more preconditions as the parent.

Answer 2

Keep in mind that IDictionary<K,V> already has that Requires :)

You can view the existing contracts DLLs for classes under: C:\Program Files (x86)\Microsoft\Contracts.

If you open mscorlib.Contracts.dll using Reflector you can view the contracts for the collection classes; CopyTo has the following:

public void CopyTo(T[] array, int arrayIndex)
{
    Contract.Requires((bool)(array != null), null, "array != null");
    Contract.Requires((bool)(arrayIndex >= 0), null, "arrayIndex >= 0");
    Contract.Requires((bool)((arrayIndex + this.Count) <= array.Length), null, "arrayIndex + this.Count  <= array.Length");
}