问题标签 [microsoft-contracts]

如何指示方法从不返回 null？目前这是我的代码。

第 19 行得到一条 Ensures notroved 消息，即使 CreateFunction 假定结果不是空的。

微软最近在 DevLabs 上发布了他们的Code Contracts框架，并获得了商业许可。我们有兴趣在我们的项目中使用它们（主要是 C#，一些 C++/CLI）来逐步替换所有自定义验证代码，但我很想知道在我们承诺之前其他人使用它的经验，具体来说：

• 您认为该框架对于大型复杂的商业项目是否足够成熟？

• 你在使用过程中遇到了什么问题？

• 你从中得到了什么好处？

• 目前是否比它的价值更痛苦？

我意识到这是一个有点主观的问题，因为它需要意见，但鉴于这个框架是 .NET 4.0 的一个非常重要的部分，并且会（可能）改变我们所有人编写验证代码的方式，我希望这个问题将被留下愿意收集有关该主题的经验，以帮助我对一个具体的、可回答的问题做出决定：

我们应该下个月开始使用它吗？

请注意，我们不提供代码 API，仅提供 Web 服务，因此对于大多数代码破坏兼容性而言，抛出的异常类型不是问题。然而，由于我希望更多的人能从这篇文章及其答案中受益，因此任何关于这个领域的细节都非常受欢迎。

我曾经使用Microsoft CodeContracts三周，现在我的一半代码只是合同。我有几十个未经证实的地方，我不能使用运行时检查，因为 IL 重写会阻止覆盖工具显示某些内容，并且编译时间少于可以接受的时间。

我不喜欢这个。现在似乎是寻求帮助的好时机。什么工具用于您的常规开发？

有没有办法向 ReSharper 表明由于按合同设计需要检查而不会发生空引用？例如，以下代码将Possible 'null' assignment to entity marked with 'NotNull' attribute在 ReSharper 中的第 7 行和第 8 行引发警告 ( )：

真正奇怪的是，如果您删除该Contract.Requires(...)行，ReSharper 消息就会消失。

更新

我通过下面的 Mike 也提到的 ExternalAnnotations 找到了解决方案。下面是如何为 Microsoft.Contracts 中的函数执行此操作的示例：

• 在ReSharper 目录Microsoft.Contracts下创建一个名为的目录。ExternalAnnotations
• 接下来，创建一个名为Microsoft.Contracts.xml并填充的文件，如下所示：

• 重新启动 Visual Studio，消息消失！

我正在尝试了解Microsoft Code Contracts库的方法，并且我具有以下简单功能：

尝试编译时，contracts 静态编译器会抛出以下警告消息：

然后立即放弃（并且不尝试进行任何进一步的合同处理）。如果我删除设置的代码，DefaultToolsVersion则合同验证程序可以正常工作，但这毫无意义，因为它会导致代码不正确。

我在谷歌上找不到任何提及...有什么方法可以解决这个问题，还是只是合同库中的一个错误？（诚​​然，它处于预发布状态）

谢谢

以下代码在前提条件下失败。这是代码合同中的错误吗？

我目前在 ASP.NET MVC 应用程序中使用Microsoft Code Contracts没有任何问题，但我似乎无法在基本的 ASP.NET 网站中完全运行它。我不完全确定它是否适用于这种类型的项目（尽管它不应该重要）所以我想把它带给每个人。

我可以很好地编译合同，但代码会跳过它们，因为我假设它没有像在其他项目类型（即 ASP.NET MVC）中那样通过属性页面启用。我已经在我的 ASP.NET 网站中访问了项目的属性页面（显示对话框而不是典型的属性页面），但它没有产生相同的菜单选项，因此没有专门的部分到代码合同。

此外，我在一个类库项目中正确启用了 Microsoft 代码合同，我用它来将我的业务逻辑与网站分开。合同编译得很好，但是当违反合同时，它会抛出一个相当无信息的"Exception of type 'System.ExecutionEngineException' was thrown"错误，没有内部异常。我的合同指定了在违规时显示的消息，但它不在例外范围内。它只是停止进程的执行（我相信这是 Microsoft 代码合同的默认功能）。

我找不到任何明确说明特定项目类型可以或不能（或不应该）与合同一起使用的地方，所以我只是想看看是否有人遇到过这个问题。

谢谢你的帮助！

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

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

我对按合同设计的概念还很陌生，但到目前为止，我很喜欢它让查找潜在错误变得多么容易。

但是，我一直在使用 Microsoft.Contracts 库（非常棒），但遇到了障碍。

以我正在尝试做的这个简化示例为例：

总而言之，我声明了一个插件遵循的接口，并要求它们声明它们的状态，并限制在任何状态下可以调用的内容。

这适用于调用站点，用于静态和运行时验证。但我不断收到的警告是“合同：确保未经证实”的Reset和Prepare功能。

我曾尝试使用Invariants 进行处理，但这并不能帮助证明Ensures约束。

关于如何通过界面证明的任何帮助都会有所帮助。

编辑1：

当我将此添加到 MyAwesomePlugin 类时：

试图暗示作为 IPlugin 的状态与我的私有状态相同，我收到相同的警告，并且警告“私有 int？number = null”行无法证明不变量。

鉴于这是静态构造函数中的第一个可执行行，我可以理解为什么它会这样说，但为什么不能证明Ensures?

编辑2

当我标记State时，[ContractPublicPropertyName("State")] 我收到一条错误消息，提示“找不到名为 'State' 且类型为 'MyNamespace.State' 的公共字段/属性”

似乎这应该让我更接近，但我并不完全在那里。

除了要求 Visual Studio Team System 能够安装带有静态检查器的 Microsoft.Contacts 之外，是否可以在没有团队系统的情况下运行静态检查器？或者，它是否依赖于工作室团队系统组件公开的 API？

另外，将静态检查器从具有团队系统的计算机复制到具有专业系统的计算机是否在许可范围内？