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