22

我可能会说我对代码合同非常熟悉：我已经阅读并理解了大部分用户手册，并且已经使用了很长时间，但我仍然有疑问。当我在 SO 中搜索“未经证实的代码合同”时，有很多点击，都在问为什么他们的具体陈述不能被静态证明。虽然我可以做同样的事情并发布我的具体场景（顺便说一句：

在此处输入图像描述),

我宁愿理解为什么任何代码合同条件都可以或不能被证明。有时我对它可以证明的东西印象深刻，有时我……嗯……礼貌地说：肯定没有留下深刻的印象。如果我想了解这一点，我想知道静态检查器使用的机制。我确信我会从经验中学习，但我会到处散布Contract.Assume声明以使警告消失，而且我觉得这不是代码合同的目的。谷歌搜索对我没有帮助，所以我想问问你们的经验：你们看到了什么（不明显的）模式？是什么让你看到了光明？

4

2 回答 2

9

你们的施工合同不满意。由于您正在引用对象的字段 (this.data)，因此其他线程可能有权访问该字段并可能在 Assume 和第一个参数解析和第三个参数解析之间更改其值。（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变量被匿名方法捕获。

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

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

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

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

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

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

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

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

于 2011-02-17T17:13:03.587 回答
5

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

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

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

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

[ContractVerification(false)]

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

我自己对代码契约的评估是，如果您只使用官方框架库并且没有大量遗留代码（例如，当开始一个新项目时），那就太好了。其他任何事情，都是快乐和痛苦的混合包。

于 2011-02-17T17:01:27.200 回答