Code contracts warnings when implementing ICollection with backing collection

Question

I've got this code:

public class MyCollection : ICollection<string>
{
    private readonly ICollection<string> _inner = new Collection<string>();

    public void Add(string item)
    {
        _inner.Add(item);
    } // <-- CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count)

    public void Clear()
    {
        _inner.Clear();
    } // <-- CodeContracts: ensures unproven: this.Count == 0

    public bool Contains(string item)
    {
        return _inner.Contains(item); // <-- CodeContracts: ensures unproven: !Contract.Result<bool>() || this.Count > 0
    }

    public void CopyTo(string[] array, int arrayIndex)
    {
        _inner.CopyTo(array, arrayIndex); // <-- CodeContracts: requires unproven: arrayIndex + this.Count  <= array.Length
    }

    public IEnumerator<string> GetEnumerator()
    {
        return _inner.GetEnumerator();
    }

    IEnumerator IEnumerable.GetEnumerator()
    {
        return GetEnumerator();
    }

    public bool Remove(string item)
    {
        return _inner.Remove(item);
    }

    public int Count
    {
        get { return _inner.Count; }
    }

    public bool IsReadOnly
    {
        get { return _inner.IsReadOnly; }
    }
}

I get these warnings:

• Add: CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count)
• Clear: CodeContracts: ensures unproven: this.Count == 0
• Contains: CodeContracts: ensures unproven: !Contract.Result<bool>() || this.Count > 0
• CopyTo: CodeContracts: requires unproven: arrayIndex + this.Count <= array.Length

How do I fix these? Is there some way to just suppress these?

Answer 1

Not sure if I follow the question but I tried the following code (implemented all required interfaces) and MyCollection myCollection = new MyCollection {"test"}; worked fine. If you are still having trouble then try to explain a little bit more what you did.

EDIT: Apart from my answer to the question I would like to make the following note for those who are making the first steps with Code Contracts.

To get the Code Contracts to show warnings Static Checking must be active (Project properties -> Code Contracts -> Perform Static Contract Checking) which is only available if Code Contract premium (not standard) edition is installed on Visual Studio 2010 Premium or on 2008 Team System.

public class MyCollection : ICollection<string>
{
    //using System;
    //using System.Collections;
    //using System.Collections.Generic;
    //using System.Collections.ObjectModel;
    //using System.Diagnostics.Contracts;

    private readonly ICollection<string> _inner = new Collection<string>();

    #region ICollection<string> Members

    public void Add(string item)
    {
        int oldCount = Count;
        _inner.Add(item);

        Contract.Assume(Count >= oldCount);
    }

    public void Clear()
    {
        _inner.Clear();

        Contract.Assume(Count == 0);
    }

    public bool Contains(string item)
    {
        bool result = _inner.Contains(item);
        // without the following assumption:
        // "ensures unproven: !Contract.Result<bool>() || this.Count > 0"
        Contract.Assume(!result || (Count > 0));

        return result;
    }

    public void CopyTo(string[] array, int arrayIndex)
    {
        Contract.Assume(arrayIndex + Count <= array.Length);
        _inner.CopyTo(array, arrayIndex);
    }

    public bool Remove(string item)
    {
        return _inner.Remove(item);
    }

    public int Count
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() == _inner.Count);
            return _inner.Count;
        }
    }

    public bool IsReadOnly
    {
        get { return _inner.IsReadOnly; }
    }

    public IEnumerator<string> GetEnumerator()
    {
        return _inner.GetEnumerator();
    }

    IEnumerator IEnumerable.GetEnumerator()
    {
        return GetEnumerator();
    }

    #endregion
}

EDIT 2:

There are some work around, choose one which best suits you:

1. Add missing Contract.Asserts as seen on above code sample;
2. Instead of implementing ICollection inherent from Collection;
3. Use StringCollection

The solutions were taken from DevLabs forum post: Problems with static checker and wrapper around generic list.

EDIT 3 (by Allrameest):

1. Added Contract.Ensures(Contract.Result<int>() == backEndCollection.Count); to the Count property which KoMet tipped about.
2. Added Contract.Assume(arrayIndex + Count <= array.Length); to the CopyTo method.
3. Removed Contract.Assert(_inner.Count == 0); from the Clear method.

Answer 2

From what I see from multiple links, you need to add this line to the Count property:

Contract.Ensures(Contract.Result<int>() == backEndCollection.Count);

Sources :

http://social.msdn.microsoft.com/Forums/en/codecontracts/thread/cadd0c05-144e-4b99-b7c3-4869c46a95a2

http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/acb3e1d8-8239-4b66-b842-85a1a9509d1e/