问题标签 [code-contracts]

结合使用代码分析和代码合同时，我收到很多警告，例如

CA1062：Microsoft.Design：在外部可见的方法“Foo.Bar(Log)”中，在使用之前验证参数“log”。

在 Foo.Bar 中，我有一个验证log.

有没有办法让 FxCop 理解代码合约？

可能重复：
我应该在 C# 中将 uint 用于不能为负数的值吗？

假设MaxValue（大约:)）2^31 与 2^32 无关紧要。一方面， usinguint看起来不错，因为它是不言自明的，它表明（并承诺？）某些值可能永远不会是负数。然而，int更常见的是，演员往往不方便。可以只使用 int 并始终使用代码协定对其进行补充（现在每个人都已迁移到 .Net 4.0，对吗？）标准库确实使用int了 forLength和Sizeproperties，即使它们永远不应该是负面的。那么，这对您来说是显而易见的，int还是比uint大多数时候更好，还是更复杂？

如果您发现这个问题没有明确说明，请提出问题。

谢谢。

编辑：是的，看起来像个骗子。但是，还有一个额外的小问题：你能给我一个很好的例子，说明在这种特殊情况下，当值可能不是负数时，如何用代码合同/断言语句补充属性/函数？

我有以下代码使用正常的数据上下文，效果很好：

但是，当我将过滤器转换为这样的扩展方法时：

我收到以下警告：

警告：CodeContracts：需要未经证实：来源！= null

我一直在玩 Code Contracts，我真的很喜欢我目前所看到的。他们鼓励我评估并明确声明我的假设，这已经帮助我确定了一些我在添加合同的代码中没有考虑过的极端情况。现在我正在尝试强制执行更复杂的不变量。我有一个案例目前无法证明，我很好奇除了简单地添加 Contract.Assume 调用之外是否还有其他方法可以解决这个问题。这是有问题的课程，为了便于阅读而被剥离：

我对如何在 ReserveSpace 中构造 Contract 调用感兴趣，以便类不变量是可证明的。特别是，它抱怨 (Length <= Buffer.Length) 和 (CurrentByte <= Length)。对我来说，它看不到满足 (Length <= Buffer.Length) 是合理的，因为它正在创建一个新缓冲区并重新分配引用。我唯一的选择是添加一个假设满足不变量吗？

我对代码合同和 linq 有疑问。我设法将问题缩小到以下代码示例。现在我被困住了。

我的 linq 链有什么问题？为什么在分析 ForPerson 调用时不重新分析“抱怨”？

编辑：ForPerson 方法的返回类型从字符串更改为 IQueryable，我的意思是。（我的错）

我终于赶上了 .NET 3.5/4.0 框架中添加的所有新内容。最近几天我一直在使用 CodeContracts，我真的很努力地喜欢它们。我很好奇其他人对 C# 中 CodeContracts 的实现有何看法？具体来说，人们如何组织诸如接口的契约类、契约不变量的契约方法等？

我喜欢合同提供的验证，乍一看它们看起来很棒。只需几行简单的代码，我什至可以在运行代码之前进行一些不错的构建检查。不幸的是，我很难克服在 C# 中实现代码契约的方式的感觉，它们使我的代码更加混乱，而不是记录契约。为了充分利用合同，我在我的代码中乱扔假设和断言等（我知道有些人会说这是一件好事）；但正如我下面的一些示例将显示的那样，它将单个简单的行变成 4 或 5 行，并且在我看来并没有真正增加替代方法（即断言、异常等）的足够价值。

目前，我最大的挫败感是：

接口合约：

这对我来说就像是一个障碍，我希望有一种更简洁的方式来记录需求，无论是通过属性还是某种形式的内置语言支持。我必须实现一个抽象类来实现我的接口，这样我才能指定合同，这一事实充其量似乎很乏味。

代码膨胀：

需要几个假设来验证现成的信息。我很感激分析器所知道的只是它在 Type 上运行，因此必须使用有限的知识，但仍然让我感到沮丧的是，一行代码需要我重写为

只是为了将事情记录在案（是的，我知道我可以使用 ContractVerificationAttribute 为方法/类等关闭此功能，或使用 SuppressMessageAttribbute 来针对特定消息，但这似乎违背了目的，因为您的代码很快就会充满抑制等。

另外，举个例子

obj 必须不为 null，并且设置为无法更改的只读字段，但我仍然需要向我的类添加“标记”方法，以便可以证明我的属性要求不返回 null：

还有更多，但我想我可能已经咆哮得够多了，我真的很感谢比我聪明得多的人的洞察力来帮助我“喜欢”代码合同并消除这种代码混乱的感觉。任何关于如何更好地构建代码、解决不稳定问题等的见解将不胜感激。

谢谢！

我有一个这样开始的方法：

GetUnboundTagsRecursively 的实现（在同一个类中实现）的合约如下所示：

静态分析器通过消息指示 ResolveTag 的标签分配行出现故障"requires unproven: source != null"。我已经看过好几次了，我不知道为什么会这样。我假设这是source对扩展方法参数的引用ToArray()。我的方法声明它确保结果不为空，所以这似乎意味着源ToArray()也不为空。我错过了什么？

附加信息：返回 IEnumerable 的方法是通过 yield return 调用实现的。我想知道枚举器的魔法是否会以某种方式弄乱代码合同......

我只是尝试更改实现以返回一个空数组而不是使用 yield return 并通过合同，所以显然这是使用 yield return 的方法的问题。有人知道解决这个问题的方法吗？

我查看了 Contracts DLL 的 IL，它实际上将合约调用放入 MoveNext() 中以实现枚举器：

这很有趣，因为 Contract.Result 调用实际上使用了错误的类型（因为 MoveNext 返回一个布尔值）。

好的，我还有另一个代码合同问题。我有一个看起来像这样的接口方法的合同（为清楚起见，省略了其他方法）：

我有使用如下界面的代码：

AddRequested需要一个非空输入参数（它实现了一个具有 Requires 合同的接口），因此在传递到AddRequested. 我是否正确使用了 ForAll 语法？如果是这样并且求解器根本不理解，是否有另一种方法可以帮助求解器识别合同，或者我是否只需要在调用 GetAllGroups() 时使用 Assume？

我一直在研究 .NET 4.0 Code Contracts 并查看 stackoverflow 以及关于此的问题。

我仍然从未遇到任何使用代码合同的示例代码，这让我想知道.. 这真的有用吗？或者也许它唯一有用的一个你的代码达到了一定的复杂性？有人在使用代码合同并且真的很高兴他们这样做了吗？

在我看来，所有代码合同都是关于方法的输入和输出的断言，此外还能够尝试找出在编译时输入和输出的值......但接下来就是这样在所有方法上都需要更多代码..值得吗？

我注意到的一个好处是，在我看来，您可以使用代码契约作为单元测试的第一行......然后当您编写单元测试时可以避免编写一些更基本的测试，因为代码契约已经涵盖了它。 。 真的吗 ？

合同是否适用于 WCF 调用？我猜不是因为您自动创建了一个代理，您无法更改。

假设我有一个public void Foo(string bar)调用者不应该使用 null 值调用的方法bar。假设我也有一个方法，调用它private void FooImpl(string bar)，它可以完成Foo. 当然，FooImpl这确实需要 的非空性bar，即使Foo是公共接口。假设我想使用 .NET 4.0 代码合同来强制执行这种非空性。

我把合同放在哪里？

如果我这样做：

然后静态检查器抱怨使用可能为空的值Foo调用FooImpl，并建议我将非空合约添加到Foo. 好的，所以我想我不能将合同检查/异常抛出委托给实现方法。

但是如果我尝试将它放在公共界面中，即：

然后静态检查器抱怨FooImpl调用Contains了一个可能为空的值——即使FooImpl在代码中调用的唯一位置是 from Foo，它本身确保它永远不会FooImpl使用空值调用。

那么，我需要两次包含同一份合同吗？还是我应该忽略静态检查器？我知道这是一种忙碌的工作来源，不应该依赖它，但我希望它有一些方法来处理这个基本的，大概是常见的场景。