Search code examples
c#collectionscode-contractspreconditions

Code Contracts 1.4.40602.0 - Contract.ForAll doesn't seem to be working?


Warning 1 CodeContracts: requires unproven: Contract.ForAll(coll, item => item != null) C:\MyApp\MyObj.cs

    public MyObj()
        : this(new Collection<Object>()) { }

    public MyObj(ICollection<Object> coll)
    {
        Contract.Requires<ArgumentNullException>(coll != null);
        Contract.Requires<ArgumentException>(Contract.ForAll(coll, item => item!= null));

        _coll = coll;
    }

I realize that in older versions of CodeContracts the Contract.ForAll() method wasn't supported, but I thought by now (ver 1.4.40602.0) it would be? Am I just doing something wrong here or is it still not supported?


Solution

  • I have no warnings with 'Warning level' set to 'low' in the CC options. With the value set to 'high' I got the warning.

    I've tried System.Collections.ObjectModel.Collection<T> and System.Collections.Generic.List<T> and both give the same warnings.

    I've tried both constructors and regular method calls - no difference.

    I've tried

    public MyObj() : this(new List<Object>()) { }
    

    and

    public MyObj() : this(new List<Object>{1}) { }
    

    and again no difference.

    Extracting a variable when doing a regular method call doesn't help either.

    Even Assume didn't help:

    public void M1()
    {
      var list = new List<Object>
        {
          1
        };
      Contract.Assume(Contract.ForAll(list, t => t != null));
      this.X(list); // Still gives warning on the ForAll requirement
    }
    
    public void X(ICollection<object> c)
    {
      Contract.Requires<ArgumentNullException>(c != null);
      Contract.Requires<ArgumentException>(Contract.ForAll(c, x => x != null));
    }
    

    (I'm using the same CC: 1.4.40602.0 on VS2010 SP1)

    UPDATE

    Worked with an array.

    Maybe, Judah Himango is right about the lack of contracts on Collection and List.