如果X<；Y和Y＝Z+1为什么X<；Z+1未被证明

本文关键字：Z+1 lt 证明 如果 为什么 | 更新日期: 2023-09-27 18:20:22

我有一个合同可以做到这一点：

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

前两个通过分析很好，但第三个说断言未经证实，一个接一个？考虑警卫。这看起来像是简单的数学。我缺什么了吗？

尝试使用字符串数组和局部值似乎效果不错。可能和长度调用有关？我试着把int换成UInt16，看看它是否是由于循环中的缓冲区溢出造成的，但也不是。

如果X<；Y和Y＝Z+1为什么X<；Z+1未被证明

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

  1. 您呼叫Contract.Assert(i < delegateParameterTypes.Length);。假设这是真的，我们继续
  2. 此时，静态分析器不知道在即将对Contract.Assert(predicate)进行的调用和上面的步骤1之间，delegateParameterTypes.Length是否发生了任何变化。你和我都知道什么都没发生，但分析器没有——尽管这两行代码是相邻的（谁能说在某个地方没有线程接触共享状态呢？）
  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与已知不会更改的值进行比较。现在，静态分析器可以对这些值的比较进行一些推断，并且应该能够证明断言。

相关文章：