代码合同 - ForAll - 静态验证支持什么

Question

静态检查有很多信息Contract.ForAll只有有限或没有支持.

我做了很多实验,发现它可以用于:

• Contract.ForAll(items, i => i != null)
• Contract.ForAll(items, p)哪里p是类型Predicate<T>

它不能用于:

• 现场访问
• 物业访问
• 方法组(我认为委托在这里被分配)
• 实例方法调用

我的问题是:

• 有哪些其他类型的代码ForAll可以使用？
• 代码合同是否经过Contract.ForAll(items, i => i != null)验证,以后在代码中从列表中取出一个项目(即通过索引)时,该项目不为空？

这是完整的测试代码:

public sealed class Test
{
    public bool Field;
    public static Predicate<Test> Predicate;

    [Pure]
    public bool Property
    {
        get { return Field; }
    }    

    [Pure]
    public static bool Method(Test t)
    {
        return t.Field;
    }

    [Pure]
    public bool InstanceMethod()
    {
        return Field;
    }

    public static void Test1()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i != null));
        Contract.Assert(Contract.ForAll(items, i => i != null)); // OK
    }

    public static void Test2()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, Predicate));
        Contract.Assert(Contract.ForAll(items, Predicate)); // OK
    }

    public static void Test3()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.Field));
        Contract.Assert(Contract.ForAll(items, i => i.Field)); // assert unproven
    }

    public static void Test4()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.Property));
        Contract.Assert(Contract.ForAll(items, i => i.Property)); // assert unproven
    }

    public static void Test5()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, Method));
        Contract.Assert(Contract.ForAll(items, Method)); // assert unproven
    }

    public static void Test6()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.InstanceMethod()));
        Contract.Assert(Contract.ForAll(items, i => i.InstanceMethod()));// assert unproven
    }
}

Answer 1

通过反编译mscorelib.dll，System.Diagnostics.Contracts我们可以很容易地看到Contract.ForAll是如何构建的：它需要集合和谓词。

public static bool ForAll<T>(IEnumerable<T> collection, Predicate<T> predicate)
{
    if (collection == null)
    {
        throw new ArgumentNullException("collection");
    }
    if (predicate == null)
    {
        throw new ArgumentNullException("predicate");
    }
    foreach (T current in collection)
    {
        if (!predicate(current))
        {
            return false;
        }
    }
    return true;
}

所以当你Contract.ForAll(items, i => i.Field)在这种情况下说i => i.Field谓词时

然后，通过在所有测试方法中遵循您的示例，我们可以看到您向Contract.ForAll方法提供了一个空列表，该方法将返回 true，因为它永远不会进入 foreach 块。

更进一步，如果您将项目添加到列表中 var items = new List<Test>() {new Test()};并再次运行测试，它将返回 false，因为public bool Field;默认情况下您的值为 false

Contract.ForAll 的目标是

确定集合中的所有元素是否存在于函数中

所以我的结论是，这与 Contarct.ForAll 无法处理某些内容无关，而是集合中至少有一个元素返回 false 或为 null