CodeContracts with collection types

Question

I have a set of children in my class, and I have an open accessor to it. I want to provide a postcondition to ensure that the elements in the collection are not null (I know that in tests 2 and 3, the caller can modify the collection, but for now, my goal is to make sure that the collection returned from the doesn property 't contain null elements).

I thought using Assume and ForAll would be enough, but that doesn't help

Here is a sample code with three classes that I tried. All three cases are absolutely identical, except that the first is ReadOnlyObservableCollection , the second is ObservableCollection , and the third is List .

- ReadOnlyObservableCollection

class Test1 { public Test1() { _children = new ObservableCollection<A>(); _childrenReadOnly = new ReadOnlyObservableCollection<A>(_children); } protected readonly ObservableCollection<A> _children; protected readonly ReadOnlyObservableCollection<A> _childrenReadOnly; public ReadOnlyObservableCollection<A> Children { get { Contract.Ensures(Contract.ForAll(Contract.Result<ReadOnlyObservableCollection<A>>(), i => i != null)); Contract.Assume(Contract.ForAll(_childrenReadOnly, i => i != null)); return _childrenReadOnly; // CodeContracts: ensures unproven: Contract.ForAll(Contract.Result<ReadOnlyObservableCollection<A>>(), i => i != null) } } [ContractInvariantMethod] private void ObjectInvariant() { Contract.Invariant(_children != null); Contract.Invariant(_childrenReadOnly != null); } } 

- ObservableCollection

 class Test2 { public Test2() { _children = new ObservableCollection<A>(); } protected readonly ObservableCollection<A> _children; public ObservableCollection<A> Children { get { Contract.Ensures(Contract.ForAll(Contract.Result<ObservableCollection<A>>(), i => i != null)); Contract.Assume(Contract.ForAll(_children, i => i != null)); return _children; // CodeContracts: ensures unproven: Contract.ForAll(Contract.Result<ObservableCollection<A>>(), i => i != null) } } [ContractInvariantMethod] private void ObjectInvariant() { Contract.Invariant(_children != null); } } 

- List

 class Test3 { protected readonly List<A> _children = new List<A>(); public List<A> Children { get { Contract.Ensures(Contract.ForAll(Contract.Result<List<A>>(), i => i != null)); Contract.Assume(Contract.ForAll(_children, i => i != null)); return _children; // No warning here when using List instead of ObservableCollection } } [ContractInvariantMethod] private void ObjectInvariant() { Contract.Invariant(_children != null); } } 

Here is the test code that uses these classes:

  Test1 t1 = new Test1(); foreach (A child in t1.Children) { child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child' } Test2 t2 = new Test2(); foreach (A child in t2.Children) { child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child' } Test3 t3 = new Test3(); foreach (A child in t3.Children) { child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child' } 

Is there any way to define a contract so that I don't write Contract.Assume(child != null) every time I use the Children property?

---

Update:

I tried to implement an Enumerator that guarantees a non-empty condition in the get Current attribute, as suggested by phoog . But the warning is still present (unexpectedly for me).

 public class NotNullEnumerable<T> : IEnumerable<T> { private IEnumerable<T> _enumerable; public NotNullEnumerable(IEnumerable<T> enumerable) { _enumerable = enumerable; } #region IEnumerable<T> Members public IEnumerator<T> GetEnumerator() { return new NotNullEnumerator<T>(_enumerable.GetEnumerator()); } #endregion #region IEnumerable Members System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator() { return GetEnumerator(); } #endregion } public class NotNullEnumerator<T> : IEnumerator<T> { private readonly IEnumerator<T> _enumerator; public NotNullEnumerator(IEnumerator<T> enumerator) { _enumerator = enumerator; } #region IEnumerator<T> Members public T Current { get { Contract.Ensures(Contract.Result<T>() != null); return _enumerator.Current; } } #endregion #region IDisposable Members public void Dispose() { _enumerator.Dispose(); } #endregion #region IEnumerator Members object System.Collections.IEnumerator.Current { get { Contract.Ensures(Contract.Result<object>() != null); return _enumerator.Current; } } public bool MoveNext() { return _enumerator.MoveNext(); } public void Reset() { _enumerator.Reset(); } #endregion } 

Use in code:

  Test1 t1 = new Test1(); var NonNullTest1 = new NotNullEnumerable<A>(t1.Children); foreach (A child in NonNullTest1) { child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child' } 

Any ideas?

Answer 1

I would create my own collection type. For example, you can implement IList<T> and “ensure” that the index getter never returns null and “requires” Add() , and the index installer never takes null as an argument.

EDIT:

To avoid the message “it is possible to call a method for a null reference” in the foreach loop, you probably also have to implement your own enumerator type and “ensure” that its Current property never returns null.

EDIT2:

Since ObservableCollection<> and ReadOnlyObservableCollection<> both decorate an instance of IList<> and therefore implement IList<> , I tried the following. Note that the inconsistency between "guarantees unproven" and "assert is false". I received the same messages whether the static type was result ReadOnlyObservableCollection<C> or IList<C> . I am using Code Contracts version 1.4.40602.0.

 namespace EnumerableContract { public class C { public int Length { get; private set; } } public class P { public IList<C> Children { get { Contract.Ensures(Contract.Result<IList<C>>() != null); Contract.Ensures(Contract.ForAll(Contract.Result<IList<C>>(), c => c != null)); var result = new ReadOnlyObservableCollection<C>(new ObservableCollection<C>(new[] { new C() })); Contract.Assume(Contract.ForAll(result, c => c != null)); return result; //CodeContracts: ensures unproven Contract.ForAll(Contract.Result<IList<C>>(), c => c != null) } } public class Program { public static int Main(string[] args) { foreach (var item in new P().Children) { Contract.Assert(item == null); //CodeContracts: assert is false Console.WriteLine(item.Length); } return 0; } } } } 

EDIT3:

Found a good summary of issues at http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/af403bbc-ca4e-4546-8b7a-3fb3dba4bb4a/ ; basically, adding additional conditions to the contract of the implemented interface violates the Liskov substitution principle, since this means that a class with additional restrictions cannot be used in any context that an object that implements this interface accepts.

Answer 2

I tried to achieve the same approach, and most of them I came:

• Declare a common INonNullable <T> interface with a single property that provides a non-empty value return; implement it in a NonNullable struct.
• Declaring INonNullEnumerator <T> and INONNullEnumable <T> interfaces (most likely it was useless) is the same as IEnumerator and IEnumerable, but INonNullEnumerable has IsEmpty property and GetEnumerator requires it to be false. NonNullEnumerator returns T, not INonNullable <T>.
• Declare my own collection that implements INonNullEnumable <T> and IList <INonNullable <T → (for compatibility with common IEnumerable and common sense), based on a NonNullable array. IList methods are explicitly implemented using INonNullable arguments, but with the same implicit methods that take T values ​​with contracts.

As a result, this hydra can be passed as a regular IEnumerable argument, returning INonNullable values ​​(which still require static checking to check for zeros, since this is a reference type), while T values ​​with a non-zero guarantee can be used in methods and in the foreach ( since foreach uses the implicit GetEnumerator () method, which returns INonNullEnumerator, which provides the return of a non-zero INonNullable, which is a NonNullable struct, and all this is supported by contracts).

But honestly, this is a monster. I coded it to try my best to conclude that the contracts guarantee that the collection does not have zeros. However, without complete success: Contract.ForAll (myList, item => item! = Null) cannot be proved just because it uses IEnumerable, neither foreach, nor my INonNullEnumerable.

My bet, this is not possible, at least with the current CodeContracts API.

Answer 3

Update your ObjectInvariant to include checks so that all items in the collections are non-zero at the end of each method call.

  [ContractInvariantMethod] private void ObjectInvariant() { Contract.Invariant(_children != null && Contract.ForAll(_children, item => item != null)); Contract.Invariant(_childrenReadOnly != null && Contract.ForAll(_childrenReadOnly, item => item != null); }