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

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

• Contract.ForAll(items, i => i != null)
• Contract.ForAll(items, p)其中 p类型为 Predicate<T>

它不能用于:

• 实地考察
• 属性(property)访问权
• 方法组(反正我觉得delegate是分配在这里的)
• 实例方法调用

我的问题是:

• 还有哪些其他类型的代码 ForAll可以一起工作吗？
• 代码契约(Contract)是否在 Contract.ForAll(items, i => i != null) 之后 promise 已证明，当稍后在代码中从列表中取出一项时(即通过索引)，该项不为空？

完整的测试代码如下:

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
    }
}

最佳答案

我找不到更多的工作表达式，事实上我发现甚至 Contract.ForAll(items, i => i != null) 也不能可靠地工作(但它理解当稍后在同一函数中的 foreach 内部使用时，item 不为空)。最后，我放弃了使用带有静态检查器的更复杂的 ForAll 契约(Contract)的可能性。

相反，我设计了一种方法来控制哪些合约用于静态检查器，哪些用于运行时检查器。我在这里介绍这种方法，希望它对对原始问题感兴趣的人有用。好处是能够编写更复杂的合约，这些合约只能在运行时进行检查，并且只为静态检查器留下易于证明的合约(并且很容易将警告保持在低计数)。

为此，需要 2 个构建 Debug(如果您还没有它们)，Debug 和 Debug + Static Contracts， Debug 构建定义了条件编译符号 MYPROJECT_CONTRACTS_RUNTIME。通过这种方式，它接收所有 Contract. 和 RtContract. 契约(Contract)。其他构建仅接收 Contract. 契约(Contract)。

public static class RtContract
{
    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Requires(bool condition)
    {
        Contract.Requires(condition);
    }

    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Ensures(bool condition)
    {
        Contract.Ensures(condition);
    }

    [Pure] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Assume(bool condition)
    {
        Contract.Assume(condition);
    }
}

public class Usage
{
   void Test (int x)
   {
        Contract.Requires(x >= 0);  // for static and runtime
        RtContract.Requires(x.IsFibonacci());  // for runtime only
   }
}

关于c# - 代码契约-ForAll-静态验证支持什么，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/30530752/