Code contracts can't prove that elment exists in list

80 Views Asked by At

Basically, I want an element added to the list if it does not already exist in it. It seems reasonable to have a post-condition that ensures that this element exists in the list after method is done. Below is minimal example which gives me error "CodeContracts: ensures unproven: _numbers.Contains(n)". Any ideas why it does not work or if there is 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);
    }
}
0

There are 0 best solutions below