How do I ensure a dictionary does not contain any null keys?

Question

   class Foo
   {
      private readonly Dictionary<int, object> _dictionary; 

      public Foo()
      {
         _dictionary = new Dictionary<int, object>();
         for (int i = 0; i < 10; i++)
         {
            _dictionary.Add(i, new object());//Just some fake data.
         }
      }

      public object Bar(int key)
      {
         Contract.Ensures(Contract.Result<object>() != null);

         return _dictionary[key];
      }
   }

I know that my dictionary contains no null values, but when I compile I get:

"CodeContracts: ensures unproven: Contract.Result<object>() != null"

I tried adding 

 "Contract.Ensures(_dictionary.Values.All(item => item != null));" in the constructor, but it didn't help.

How can I communicate to the CodeContract system that _dictionary[key] can't return null?

Answer 1

Hi,

Specifying Ensures in the constructor wouldn't be enough.  You'd need to specify an invariant contract, if it were possible.  Contract.ForAll would be nice but it doesn't seem to work.  Furthermore, as an invariant it causes additional unproved warnings in every method, so it probably wouldn't be worth it anyway.

I always use Contract.Assume for this, though I know it's not ideal:

var result = _dictionary[key];

Contract.Assume(result != null);

return result;

Alternatively, you could create a wrapper class to define the non-null contract as follows.  Then you can be confident with the assumption.

Note that in the following example I purposefully don't derive from IDictionary<TKey, TValue> because its contract allows null values and Code Contracts disallows strengthening preconditions when implementing an interface.

using System.Collections.Generic;
using System.Diagnostics.Contracts;

namespace CCTest
{
	class ElementsNotNull
	{
		private readonly NonNullDictionary<int, object> _dictionary = new NonNullDictionary<int, object>();

		public ElementsNotNull()
		{
			for (int i = 0; i < 10; i++)
			{
				_dictionary.Add(i, new object());
			}
		}

		[ContractInvariantMethod]
		[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Performance", "CA1822:MarkMembersAsStatic", Justification = "Required for code contracts.")]
		private void ObjectInvariant()
		{
			Contract.Invariant(_dictionary != null);
		}

		public object Bar(int key)
		{
			Contract.Ensures(Contract.Result<object>() != null);

			return _dictionary[key];		// No warnings
		}
	}

	class NonNullDictionary<TKey, TValue> : IEnumerable<KeyValuePair<TKey, TValue>>
		where TValue : class
	{
		public TValue this[TKey key]
		{
			get
			{
				Contract.Ensures(Contract.Result<TValue>() != null);

				var value = dictionary[key];

				Contract.Assume(value != null);

				return value;
			}
			set
			{
				Contract.Requires(value != null);

				dictionary[key] = value;
			}
		}

		private readonly Dictionary<TKey, TValue> dictionary = new Dictionary<TKey, TValue>();

		public void Add(TKey key, TValue value)
		{
			Contract.Requires(value != null);

			dictionary.Add(key, value);
		}

		public IEnumerator<KeyValuePair<TKey, TValue>> GetEnumerator()
		{
			return dictionary.GetEnumerator();
		}

		System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator()
		{
			return dictionary.GetEnumerator();
		}
	}
}

- Dave

---

http://davesexton.com/blog

Answer 2

Hmm. That's an interesting approach. I'm not sure how I feel about the Contract.Assumes (kind of feels like cheating) but the invariant stuff is interesting.

I found another solution, though it's also a bit hacky.

      public object Bar(int key)
      {
         Contract.Ensures(Contract.Result<object>() != null);

         object ret = _dictionary[key];
         if(ret == null)
         {
               throw new Exception("I will never be thrown.");
         }
         return ret;
      }

It gets the job done, but on a higher level I feel like adding superfluous code just to satisfy code contracts kind of makes the whole code contracts thing counterproductive. It's a quandary.

Answer 3

Hi, 

All you're doing there is making the assumption explicit in a strange way.  It's more straightforward to use Contract.Assume.  That's what it's for :)

- Dave

---

http://davesexton.com/blog