代码收缩,如果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-QED methodParameters，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与已知不会改变的值进行比较。现在，静态分析器可以对这些值的比较做出一些推断，并且应该能够证明这些断言。