Code contracts cannot prove elment exists in the list

Basically, I want the item to be added to the list if it doesn't already exist in it. It seems sensible to have a post-condition to ensure that this item exists in the list after the method completes. Below is a minimal example that gives me the error "CodeContracts: Provides Unproven: _numbers.Contains (n)". Any ideas why this isn't working or is there a way to rewrite the code to make it work?

class Test
{
    private List<int> _numbers = new List<int>();

    public void Add(int n)
    {
        Contract.Ensures(_numbers.Contains(n));
        if (!_numbers.Contains(n))
        {
            _numbers.Add(n);
        }
    }
    [ContractInvariantMethod]
    void ObjectInvariants()
    {
        Contract.Invariant(_numbers != null);
    }
}

      

+3


source to share





All Articles