How to use code contracts when receiving interfaces such as IDictionary <T, U>?

Question

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

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

The ' LuaDictionary.CopyTo(KeyValuePair<String,Object>[],Int32) ' method implements the ICollection<KeyValuePair<String,Object>>.CopyTo(KeyValuePair<String,Object>[],Int32) 'interface method, so you cannot add Requires .

I see that there are some related questions, but they all seem to be related to user-controlled interfaces. Obviously, IDictionary<T, U> not under my control, so I cannot annotate it using ContractClassFor or something like that.

I just can't use code contracts here? If so ... a big bummer ...

Answer 1

This is a bummer, but understandable, because client code that uses instances of your class as IDictionary<string, object> must not meet the prerequisites that are not expected from IDictionary<string, object> .

You can read the answer provided to this SO question , which references and quotes the Code Contracts User Guide, and you can look at this article explaining the situation this way, and a simple example follows:

Please note that the Liskov signature principle is valid for code contracts in much the same way as for simple classes. The Liskov principles state the following:

Subclasses should always be substituted for base classes.

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

Answer 2

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

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

If you open mscorlib.Contracts.dll with the help of 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"); }