c# - 代码契约(Contract)，如果 X < Y 且 Y = Z+1 为什么 X < Z+1 未被证明

Question

我有一个合约是这样做的:

for (int i = 0; i < delegateParameterTypes.Length; i++)
{
    Contract.Assert(i < delegateParameterTypes.Length);
    Contract.Assert(delegateParameterTypes.Length == methodParameters.Length + (1));
    // Q.E.D.
    Contract.Assert(i < methodParameters.Length + (1));
}

前两次通过分析很好，但第三次说断言未经证实，差了一个？考虑后卫。这似乎是简单的数学。有什么我想念的吗？

用字符串数组和本地值尝试它似乎工作正常。可能与 .Length 调用有关？我尝试将 int 交换为 UInt16 以查看它是否是由于循环中的缓冲区溢出引起的，但也不是。

Answer 1

嗯，我唯一能想到的是静态分析器对这些断言有问题。关注我:

1. 您调用 Contract.Assert(i < delegateParameterTypes.Length); .假设这是真的，我们继续。
2. 此时，静态分析器不知道关于delegateParameterTypes.Length 是否有任何改变。在即将发生的通话之间 Contract.Assert(predicate)和上面的步骤 1。你和我都知道什么都没发生，但分析器却不知道——尽管这两行代码是相邻的(谁能说那里没有某个线程接触共享状态？)
3. 您调用下一个电话:Contract.Assert(delegateParameterTypes.Length == methodParameters.Length + (1));分析仪对此进行了检查，这也是正常的。
4. 此时，分析器不知道关于delegateParameterTypes 是否有任何改变。或 methodParameters --QED，断言未经证实 Contract.Assert(i < methodParameters.Length + (1));在下一行。

同样，可能有一些与这些事物相关的共享全局状态，并且该状态可能在两次调用 Contract.Assert 之间发生了变化。 .请记住，对你我来说，代码看起来是线性和同步的。现实是或可能完全不同，静态分析器不能对这些对象在连续调用 Contract.Assert 之间的状态做出任何假设。 .

然而，什么可能有效:

int delegateParameterTypesLength = delegateParameterTypes.Length;
int methodParametersLength = methodParameters.Length + 1;

for (int i = 0; i < delegateParameterTypesLength; i++)
{
    Contract.Assert(delegateParameterTypesLength == methodParametersLength);
    // QED
    Contract.Assert(i < methodParametersLength);
}

通过将长度分配给变量，静态分析器现在可以知道这些值在 for 内不会改变。循环，或分配它们的方法的外部。现在你正在比较 i具有已知不会更改的值。现在，静态分析器可以对这些值的比较做出一些推断，并且应该能够证明断言。