c# - CodeContracts 无法证明简单的保证

Question

我有一个类似这样的结构:

public struct Test
{
  public int x;
  public int y;

  public static bool AreEqual(Test lhs, Test rhs)
  {
    Contract.Ensures(Contract.Result<bool>() == ((lhs.x == rhs.x) && (lhs.y == rhs.y)));
    return (lhs.x == rhs.x) && (lhs.y == rhs.y);
  }

  public static bool AreNotEqual(Test lhs, Test rhs)
  {
    Contract.Ensures(Contract.Result<bool>() == !((lhs.x == rhs.x) && (lhs.y == rhs.y)));
    return !AreEqual(lhs, rhs);
  }
}

证明 AreEqual 的 Ensures 没有问题，但不能证明 AreNotEqual 的 Ensures。

如果 Ensures 条件从 A == B 形式更改为 !A || B 和 !B || A，逻辑上是等价的，没问题，就是冗长多了，可读性差了很多。

同样，如果我只是放入相等逻辑而不是 !AreEqual(lhs, rhs)，没关系，但同样，我宁愿不必放入重复。

我的问题是:为什么 CodeContracts 静态分析器不能处理简单的否定？是否有什么我遗漏的微妙之处意味着它实际上无法推断？

作为奖励问题:是否有关于分析器实际做什么/可以做什么的任何文件？有时看起来很有能力，然后在像这个例子这样看似简单的事情上失败。在试图证明这些事情时，很高兴知道它的“思维过程”是什么。

Answer 1

我不知道可以回答奖励问题的文档。我也无法具体回答为什么它不能证明所写的后置条件，但如果您的最终目标只是减少相等逻辑的重复，这可能会有所帮助。

这些方法不会导致可见的状态变化，因此可以使用 [Pure] 属性进行标记。此时，AreNotEqual 中的.Ensures 可以直接引用AreEqual。然后静态分析器有足够的信息，您只有用 AreEqual 表示的相等逻辑。

public struct Test
{
    public int x;
    public int y;

    [Pure]
    public static bool AreEqual(Test lhs, Test rhs)
    {
        Contract.Ensures(Contract.Result<bool>() == ((lhs.x == rhs.x) && (lhs.y == rhs.y)));
        return (lhs.x == rhs.x) && (lhs.y == rhs.y);
    }

    [Pure]
    public static bool AreNotEqual(Test lhs, Test rhs)
    {
        Contract.Ensures(Contract.Result<bool>() == !AreEqual(lhs, rhs));
        return !AreEqual(lhs, rhs);
    }
}

// CodeContracts: Checked 4 assertions: 4 correct