3

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);
    }
}
Knowledge Cube
  • 990
  • 12
  • 35
user1242967
  • 1,220
  • 3
  • 18
  • 30
  • I tried the code above and it seems to run perfect. I have negated the contracts just to prove they are running and they throw errors as expected. What version of visual studio are you running? – Jake Matthews May 18 '17 at 20:50
  • I am running it on VS15. What do you mean that when running this code errors get thrown as expected? Is the code I wrote is actually incorrect and errors should be thrown? – user1242967 May 19 '17 at 10:46
  • Sorry for not being clear, I meant I changed 'Contract.Ensures( _numbers.Contains(n) );' to 'Contract.Ensures( ! _numbers.Contains(n) );' and an error was thrown as it should do. I think your code in correct (Worked for me on VS15). – Jake Matthews May 19 '17 at 10:50
  • Maybe your code contracts is not update? In the project properties, what code contract settings have you selected? – Jake Matthews May 19 '17 at 10:52

0 Answers0