"I have a custom Dictionary wrapper class" - that implements IDictionary<TKey, TValue>. Interface methods can specify contracts, and the class methods that implement them must meet the contracts. In this case, IDictionary<TKey, TValue>.ContainsKey(TKey) has the contract you're asking about:
Contract.Ensures(!Contract.Result<bool>() || this.Count > 0);
Logically, !a || b can be read as a ===> b (a implies b), and using that, we can translate this to English:
If ContainsKey() returns true, the dictionary must not be empty.
This is a perfectly sensible requirement. An empty dictionary must not claim to contain keys. This is what you need to prove.
Here's a sample DictionaryWrapper class that adds Contract.Ensures to promise that the implementation detail of Count being equal to innerDictionary.Count is a hard guarantee that other methods can rely upon. It adds a similar Contract.Ensures to ContainsKey so that the IDictionary<TKey, TValue>.TryGetValue contract is also verifiable.
public class DictionaryWrapper<TKey, TValue> : IDictionary<TKey, TValue>
{
IDictionary<TKey, TValue> innerDictionary;
public DictionaryWrapper(IDictionary<TKey, TValue> innerDictionary)
{
Contract.Requires<ArgumentNullException>(innerDictionary != null);
this.innerDictionary = innerDictionary;
}
[ContractInvariantMethod]
private void Invariant()
{
Contract.Invariant(innerDictionary != null);
}
public void Add(TKey key, TValue value)
{
innerDictionary.Add(key, value);
}
public bool ContainsKey(TKey key)
{
Contract.Ensures(Contract.Result<bool>() == innerDictionary.ContainsKey(key));
return innerDictionary.ContainsKey(key);
}
public ICollection<TKey> Keys
{
get
{
return innerDictionary.Keys;
}
}
public bool Remove(TKey key)
{
return innerDictionary.Remove(key);
}
public bool TryGetValue(TKey key, out TValue value)
{
return innerDictionary.TryGetValue(key, out value);
}
public ICollection<TValue> Values
{
get
{
return innerDictionary.Values;
}
}
public TValue this[TKey key]
{
get
{
return innerDictionary[key];
}
set
{
innerDictionary[key] = value;
}
}
public void Add(KeyValuePair<TKey, TValue> item)
{
innerDictionary.Add(item);
}
public void Clear()
{
innerDictionary.Clear();
}
public bool Contains(KeyValuePair<TKey, TValue> item)
{
return innerDictionary.Contains(item);
}
public void CopyTo(KeyValuePair<TKey, TValue>[] array, int arrayIndex)
{
innerDictionary.CopyTo(array, arrayIndex);
}
public int Count
{
get
{
Contract.Ensures(Contract.Result<int>() == innerDictionary.Count);
return innerDictionary.Count;
}
}
public bool IsReadOnly
{
get
{
return innerDictionary.IsReadOnly;
}
}
public bool Remove(KeyValuePair<TKey, TValue> item)
{
return innerDictionary.Remove(item);
}
public IEnumerator<KeyValuePair<TKey, TValue>> GetEnumerator()
{
return innerDictionary.GetEnumerator();
}
IEnumerator IEnumerable.GetEnumerator()
{
return innerDictionary.GetEnumerator();
}
}
