CodeContracts cannot prove a simple ensures

Question

I have a struct similar to this:

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

It has no problem proving the Ensures for AreEqual, but it can't prove the one for AreNotEqual.

If the Ensures conditions are changed from the form A == B to !A || B and !B || A, which is logically equivalent, it has no problem, but that's far more verbose and less readable.

Likewise, if I just put the equality logic in instead of !AreEqual(lhs, rhs), it's ok, but again, that's repetition I'd rather not have to put in.

My question is: Why can't the CodeContracts static analyser cope with a simple negation? Is there something subtle I'm missing that means it actually can't be inferred?

As a bonus question: Is there documentation anywhere of what the analyser actually does/can do? It seems quite capable sometimes, then fails at something seemingly simple like this example. It'd be nice to know what its "thought process" is when trying to prove these things.

Answer 1

I am unaware of documentation that would answer the bonus question. I also cannot specifically answer why it can't prove the postconditions as written, but if your end goal is simply to reduce duplication of the equality logic, this might help.

The methods result in no visible state changes, and can therefore be marked with the [Pure] attribute. At that point, the .Ensures in AreNotEqual can refer to AreEqual directly. The static analyzer then has enough information, and you only have equality logic expressed in 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