基本上,如果列表中尚不存在一个元素,我希望将其添加到列表中。在方法完成后有一个后置条件来确保该元素存在于列表中似乎是合理的。下面是一个最小的例子,它给了我错误“CodeContracts:确保未经证实:_numbers.Contains(n)”。有什么想法为什么它不起作用,或者是否有办法重写代码以使其起作用?
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);
}
}