问题标签 [code-contracts]

我正在玩微软的 CodeContracts，遇到了一个我无法解决的问题。我有一个有两个构造函数的类：

该示例已简化。我不知道如何检查第二个构造函数f是否 > 0。这甚至可以通过合同实现吗？

我在 Visual Studio 2010 中的代码合同工作正常，但我无法ccrewrite.exe从命令行做任何有用的事情。这是一个示例应用程序：

然后我编译代码并在其上运行 ccrewrite.exe：

之后就没有RewrittenDummy.exe文件了。

我已经尝试了很多选项，但没有任何区别。我注意到的几件事：

• 它肯定在加载 Dummy.exe，因为如果我指定一个不存在的文件，它就会死掉
• Dummy.exe 肯定包含对 Contract 的引用——如果我在没有参数的情况下运行它，它会适当地失败（但如果它被重写，错误消息没有像我预期的那样被填写）
• 使用后置条件和不变量没有区别

我试过调高警告和冗长，但这根本没有帮助我做错了什么？

（也在代码合同论坛中作为问题提出。我将自己在这里添加任何相关答案。）

我试图在代码合同中演示不变量，我想我会举一个字符串排序列表的例子。它在内部维护一个数组，有用于添加等的备用空间 - 基本上就像List<T>. 当它需要添加一个项目时，它将它插入到数组中，等等。我想我有三个不变量：

• 计数必须是合理的：非负数并且最多与缓冲区大小一样大
• 缓冲区未使用部分中的所有内容都应为空
• 缓冲区已用部分中的每个项目都应至少与之前的项目一样“大”

现在，我尝试以这种方式实现它：

不幸ccrewrite的是，正在搞乱循环。

用户文档说该方法应该只是对Contract.Invariant. 我真的必须像这样重写代码吗？

这有点难看，尽管它确实有效。（这比我之前的尝试要好得多，请注意。）

我的期望不合理吗？我的不变量不合理吗？

（也在代码合同论坛中作为问题提出。我将自己在这里添加任何相关答案。）

（也发布在 MSDN 论坛上- 但据我所知，这并没有获得太多流量。）

我一直在尝试提供Assertand的示例Assume。这是我得到的代码：

（当然，能够传入空引用而不是现有Random引用的业务纯粹是教学。）

我曾希望，如果检查员知道这一点firstRoll并且secondRoll每个人都在范围内[1, 6]，那么它能够计算出总和在范围内[2, 12]。

这是不合理的希望吗？我意识到这是一项棘手的工作，确切地计算出可能发生的事情......但我希望检查员足够聪明:)

如果现在不支持，这里有没有人知道它是否可能在不久的将来得到支持？

编辑：我现在发现静态检查器中有非常复杂的算术选项。使用“高级”文本框，我可以从 Visual Studio 中试用它们，但据我所知，它们的作用没有像样的解释。

当我注意到来自我的 Visual Studio (2008) 内部的静态验证警告时，我只是在 Stack Overflow 上胡乱回答某人的问题：

我收到消息需要未经证实的来源！= null。在我看来，情况并非如此。这当然只是一个例子。另一方面，一些非常漂亮的东西似乎运作良好。

我正在使用 1.2.20518.12 版本（5 月 18 日）。我发现代码合同很有趣，但其他人有过这样的案例吗？您认为当前的实现在实践中是可用的，还是在这一点上认为它们纯粹是学术性的？

我已经把它变成了一个社区维基，但我想听听一些意见:)

我说的是那些最终会出现在 .NET 4.0 中的代码合同。他们使用什么二进制重写器来注入使其全部工作的代码并且它是公开可用的？我希望它不仅仅是一个编译器，因为我希望能够将他们的二进制重写器用于 AOP。

例如本文介绍了它们。

有什么好处？

静态分析看起来很酷，但同时它会阻止在单元测试中将 null 作为参数传递的能力。（如果您按照文章中的示例进行操作）

在单元测试的话题上——考虑到现在的情况，如果你已经练习过自动化测试，那么代码合同肯定没有意义吗？

更新

玩过 Code Contracts 我有点失望。例如，根据接受答案中的代码：

对于单元测试，你还是要写测试保证null不能通过，如果合约是业务逻辑，结果大于等于0 。换句话说，如果我要删除第一个合同，任何测试都不会中断，除非我专门对此功能进行了测试。然而，这是基于不使用更好（终极等）版本的 Visual Studio 中内置的静态分析。

从本质上讲，它们都归结为编写传统 if 语句的另一种方式。我实际使用TDD 和 Code Contracts的经验说明了为什么，以及我是如何去做的。

我正在尝试 .net 3.5 的 .net 代码合同 我有一些单元测试，我正在运行 PartCover 来计算代码覆盖率。

PartCover 一直在我的报告中包含 System.Diagnostics.Contracts。以下是我用来包含 MyProject 并排除其他所有内容的规则。

有什么建议么？

对于我的所有 LINQ 语句，代码合同不断给我“可能在空引用上调用方法”警告，我找不到使它们静音的方法。例如，以下方法会生成两个这样的警告，因为我正在访问“car”对象的“Make”和“Model”属性，而没有先检查 null。

在我的特殊情况下，我知道 Cars 集合永远不会包含任何空条目，所以我想我可以在方法中添加一个 Assume 以使静态检查器静音，如下所示：

但这不起作用，大概是因为期望静态检查器能够理解有点过分。因此，我决定使用以下 SuppressMessage 属性来抑制警告：

但由于某种原因，这无法抑制警告。我什至还尝试了以下 SuppressMessage 属性，但均无效：

我什至尝试使用 ContractVerification 属性完全禁用该方法的合同验证：

但这也没有用。所以，我决定在 LINQ 语句的“where”子句中添加一个显式的空检查：

这成功地消除了“where”子句的警告，但并没有消除“select”子句的警告。事实上，我发现真正摆脱这两个警告的唯一方法是在 LINQ 语句中的每个子句中添加空检查，如下所示：

显然，这不是很干净或高效的代码，而且我实际上并不打算在我的所有 LINQ 语句中添加这种冗余的空检查——尤其是当我知道枚举不包含任何空条目时。这个问题的最佳解决方案是让静态检查器理解 Contract.Assume 确保集合中每个项目的非空值的语句，但如果无法做到，那么至少尊重方法上的 SuppressMessage 属性.

我一直在 VS2008 ( http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx )上玩代码合同。
它们肯定很好，并且为方法内部的 if-then-throw 检查提供了可靠的替代方案。

尽管如此，我一直希望它们能够满足我强烈认为不可为空的引用类型的需求。
唉，据我所见，情况似乎并非如此。
这是我的理解：

• 这样的事情仍然会在运行时引起问题：
  MyClass a = null;
a.ToString();

• 我仍然必须明确地编写检查，即使是以更简洁和流线型的方式。

• 除非您使用 VS Team System，否则您只能在运行时使用代码契约来检查事物，在编译时没有任何好处。
  这意味着当出现问题时，您仍然必须处理事情。
  与处理简单的异常没有太大区别。

• 即使使用 VSTS 静态分析也不如在运行时完成的那样好。
  这是完全可以理解的，但它仍然是此功能适用于运行时使用的另一个迹象。

如果我错了，请纠正我，但据我所知，代码合同无法让我的生活更轻松，我的程序更健壮，就像不可为空的引用类型一样。

不要误会我的意思，我不喜欢代码合同。
它们是对整个框架的一个非常好的增强。
只是如果这不能填补 C# 由于没有不可为空的引用类型而留下的空白，那么在这一点上恐怕什么都不会。
你怎么看？