C# 代码契约：什么可以静态证明，什么不能？

Question

我可能会说我对代码合同非常熟悉：我已经阅读并理解了大部分 用户手册并且已经使用它们很长一段时间了，但我仍然有疑问。当我搜索“未经验证的代码合约”时，有相当多的点击，所有这些都询问为什么他们的特定声明无法被静态证明。尽管我可以做同样的事情并发布我的具体场景（顺便说一句：

),

我更愿意理解为什么任何代码合同条件可以或无法证明。有时我对它所证明的东西印象深刻，有时我……好吧……礼貌地说：绝对不印象深刻。如果我想理解这一点，我想知道静态检查器使用的机制。我确信我会通过经验学习，但我在各处喷洒 Contract.Assume 语句以使警告消失，而且我觉得这不是代码契约的用途。谷歌搜索对我没有帮助，所以我想问问你们的经验：你们看到了什么（不明显的）模式？是什么让你看到了光明？

Answer 1

你们的施工合同没有得到满足。由于您正在引用对象的字段 (this.data)，因此其他线程可能有权访问该字段，并且可能会在假设和第一个参数解析和第三个参数解析之间更改其值。 （ei，它们可能是三个完全不同的数组。）

您应该将数组分配给局部变量，然后在整个方法中使用该变量。然后分析器将知道约束得到满足，因为没有其他线程能够更改引用。

var localData = this.data;
if (localData == null) return;
byte[] newData = new byte[localData.Length]; // Or whatever the datatype is.
Array.Copy(localData, newData, localData.Length); // Now, this cannot fail.

这具有额外的好处，不仅满足约束，而且实际上使代码在许多情况下更加健壮。

我希望这能让您找到问题的答案。我实际上无法直接回答您的问题，因为我无法访问包含静态检查器的 Visual Studio 版本。 （我使用的是 VS2008 Pro。）我的答案是基于我自己对代码的目视检查得出的结论，并且静态合同检查器似乎使用了类似的技术。我很着迷！我需要给自己找一个。 :-D

更新： （有很多猜测）

经过反思，我认为我可以很好地猜测什么可以被证明或不能被证明（即使无法访问静态检查器）。正如另一个答案中所述，静态检查器不进行过程间分析。因此，随着多线程变量访问的迫在眉睫（如在OP中），静态检查器只能有效地处理局部变量（如下定义）。

我所说的“局部变量”是指不能被任何其他线程访问的变量。这将包括在方法中声明或作为参数传递的任何变量，除非参数用 ref 或 out 修饰，或者变量是在匿名方法中捕获的。

如果局部变量是值类型，那么它的字段也是局部变量（递归地依此类推）。

如果局部变量是引用类型，则只有引用本身（而不是其字段）可以被视为局部变量。即使对于在方法内构造的对象也是如此，因为构造函数本身可能会泄漏对构造对象的引用（例如，用于缓存的静态集合）。

只要静态检查器不进行任何过程间分析，对上述定义的非局部变量所做的任何假设都可以随时失效，因此在静态分析中会被忽略。

例外 1：由于运行时已知字符串和数组是不可变的，因此只要字符串或数组变量本身是本地的，它们的属性（例如长度）就可以进行分析。这不包括可由其他线程可变的数组内容。

例外 2：运行时可能知道数组构造函数不会泄漏对构造数组的任何引用。因此，在方法主体内构造且未泄漏到方法外部（作为参数传递给另一个方法、分配给非局部变量等）的数组具有也可以被视为局部变量的元素。

这些限制看起来相当繁重，我可以想象有几种方法可以改进，但我不知道已经做了什么。理论上，静态检查器可以完成以下一些其他事情。手头有它的人应该检查一下已经做了什么和没有做什么：

• 它可以确定构造函数是否不会泄漏对对象或其字段的任何引用，并将如此构造的任何对象的字段视为局部变量。
• 可以对其他方法进行无泄漏分析，以确定在该方法调用之后传递给方法的引用类型是否仍然可以被认为是本地的。
• 用 ThreadStatic 或 ThreadLocal 修饰的变量可以被视为局部变量。
• 可以给出选项来忽略使用反射修改值的可能性。这将允许引用类型上的私有只读字段或静态私有只读字段被视为不可变。此外，当启用此选项时，私有或内部变量 X 仅在 lock(X){ /**/ } 构造中被访问过，并且不是leaked 可以被认为是局部变量。然而，这些东西实际上会降低静态检查器的可靠性，所以这有点不确定。

另一种可能开启大量新分析的可能性是以声明方式将变量和使用它们的方法（等等递归地）分配给特定的唯一线程。这将是对该语言的重大补充，但可能是值得的。

Answer 2

简而言之，静态代码分析器似乎非常有限。例如，它不会检测

readonly string name = "I'm never null";

为不变量。从我在 MSDN 论坛上收集到的信息来看，它会自行分析每种方法（出于性能原因，而不是人们认为它会变得更慢），这限制了它在验证代码时的知识。

为了在证明正确性的学术崇高目标和能够完成工作之间取得平衡，我诉诸于装饰单个方法（甚至根据需要甚至是类），

[ContractVerification(false)]

而不是在逻辑中撒上大量假设。这可能不是使用 CC 的最佳实践，但它确实提供了一种无需取消选中任何静态检查器选项即可消除警告的方法。为了不丢失此类方法的前置/后置条件检查，我通常添加具有所需条件的存根，然后调用排除的方法来执行实际工作。

我自己对代码契约的评估是，如果您仅使用官方框架库并且没有大量遗留代码（例如，在开始新项目时），那么它非常好。任何其他的事情都是快乐和痛苦的混合体。