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

Question

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

22

我已经相当熟悉代码合同了：我已经阅读并理解了大部分用户手册，并且已经使用它们相当长时间，但我仍然有问题。当我在搜索SO中输入“code contracts unproven”时，会出现很多结果，所有这些结果都在问为什么他们的特定语句无法被静态证明。尽管我也可以这样做并发布我的具体方案（顺便说一下：

），

但我更想了解为什么任何一个代码合同条件都可以或不能被证明。有时我对它所能证明的东西感到印象深刻，有时候......嗯......委婉地说：完全没有印象。如果我想要理解这个问题，我想知道静态检查器使用的机制。我相信我会通过经验学习，但我正在到处添加Contract.Assume语句以消除警告，我觉得这不是代码合同的初衷。谷歌并没有帮助我，因此我想向您询问您的经验：您见过什么（不明显的）模式？是什么让您看到了光明？

- JBSnorro

非常好的问题，但我想知道是否有一个单一的答案。静态检查器仍在每个发布版本中不断改进。 - koenmetsu

如果每次发布都没有改进，那就太奇怪了，因为还有很多需要改进的地方... :( - JBSnorro

2个回答

5

简短回答是静态代码分析器似乎非常有限。例如，它无法检测到：

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

作为不变量。根据我在MSDN论坛上的了解，它会单独分析每个方法（出于性能原因，尽管人们认为它不可能变得更慢），这限制了它在验证代码时的知识。

为了在追求正确性和完成工作之间取得平衡，我已经开始使用修饰单个方法（或甚至是类，如果需要）的方式。

[ContractVerification(false)]

与其在逻辑中添加许多假设，不如将其集中处理。虽然这可能不是使用CC的最佳实践，但它确实提供了一种摆脱警告而不取消任何静态检查器选项的方法。为了不失去这些方法的前/后置条件检查，我通常会添加一个带有所需条件的存根，然后调用被排除的方法以执行实际操作。

我个人对代码合约的评估是，如果您只使用官方框架库并且没有太多的旧代码（例如，在启动新项目时），那么它非常好。否则，它就是一种令人愉快和痛苦并存的混合体。

- Morten Mertner

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Jeffrey L Whitledge · Accepted Answer

你的构造函数中的合同没有得到满足。由于你正在引用一个对象的字段（this.data），其他线程可能会访问该字段，并在假设和第一个参数解析以及第三个参数解析之间更改其值。（例如，它们可能是三个完全不同的数组。）

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

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：由于字符串和数组在运行时被认为是不可变的，因此它们的属性（如 Length）可以被分析，只要字符串或数组变量本身是本地变量即可。这不包括其他线程可变的数组内容。

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

这些限制似乎相当严厉，我可以想象几种改进的方法，但我不知道已经完成了什么。以下是静态检查器理论上可以完成的其他一些事情。有这个工具的人应该检查已经完成了什么，还有哪些没有完成：

此功能可以确定构造函数是否泄漏了任何对对象或其字段的引用，并将所构造的任何对象的字段视为局部变量。
可以对其他方法进行无泄漏分析，以确定传递给方法的引用类型在该方法调用后是否仍然可以被视为局部变量。
使用ThreadStatic或ThreadLocal修饰的变量可以被视为局部变量。
可以提供选项来忽略使用反射修改值的可能性。这将允许将引用类型上的私有只读字段或静态私有只读字段视为不可变。另外，当启用此选项时，仅在lock(X){ /**/ }结构内部访问的一个私有或内部变量X且未泄漏的情况下，该变量可以被视为局部变量。但是，这些事情实际上会降低静态检查器的可靠性，因此有点棘手。

另一个可能会开启许多新分析的可能性是将变量和使用它们的方法（以及递归地如此）声明地分配到特定的唯一线程。这将是语言的重大改进，但可能值得一试。