.NET 4代码合同：“要求未经证实：源！= null”

Question

我刚开始在我的项目中使用代码合同。然而，我的存储库实现存在问题，它使用Entity Framework查询我的数据库。

我有以下方法：

public IEnumerable<Organization> GetAllOrganizations()
{
    return _uow.CreateSet<Party>().OfType<Organization>().AsEnumerable();
}

该方法返回一个集合，其中包含数据库中的所有组织，或者如果数据库中没有组织，则返回一个空集合。

然而，根据CodeContracts，这不是可以接受的，因为它会给我一个错误："requires unproven: source != null"。

它想要告诉我什么？我可以使用Contract.Assume满足代码合同，假设它总是能找到某些东西，但是那样我需要在从数据库读取数据的所有方法中这样做。

我是否遗漏了一些内容，或者这是在使用数据库和LINQ时预期的行为？

- Vern

---

什么是“源代码”？你所调用的方法中是否有合同？ - Anon.

这个问题有帮助吗？链接 - adrianbanks

@Anon：我不知道“source”是什么。我不知道实体框架中的方法是否有合同，但我认为没有。@adrianbanks：不好意思，我看不出那怎么能帮助我。 - Vern

Answer 1

我的猜测是，CreateSet、OfType和AsEnumerable方法中的一个被声明为带有名为"source"的this参数的扩展方法，而CodeContracts无法证明它不为空。此外，在进入时，您是否需要添加Requires子句来指定_uow非空？

由于CreateSet在MSDN中未出现，因此似乎是扩展方法。如果该方法永远不应返回null，则可以通过将此合同添加到CreateSet来强制执行：

Contract.Ensures(Contract.Result<T>() != null);

当CodeContracts分析器看到这个规则时，它将把它视为输入OfType不会为空的证明，警告应该消失。

- dc42

---

很可能是 AsEnumerable，它有一个 source != null 的前置条件。我不确定在 Entity Framework 中的方法是否有许多（或任何）合约，因此 CreateSet 和 OfType 上都没有后置条件。你可能需要创建自己的包装函数。 - porges

只有在代码的调用者负责满足前置条件时，才能设置前置条件。在这种情况下，似乎 _uow 是内部责任，而不是调用者的责任。 - koenmetsu

你说得对，我需要一个Requires条款来指定_uow是非空的。但是添加了这个之后，我仍然收到错误信息。@Porges：我认为你关于AsEnumerable是原因的说法是正确的。我已经对AsEnumerable进行了一些测试，并且在这里也遇到了问题。似乎为许多函数编写包装器函数是一项相当繁琐的任务 - 尤其是在使用不使用代码合同的第三方API时。我将不得不重新考虑是否要使用代码合同。 - Vern

@Vern：是的，我认为一个重要的功能就是让用户能够在第三方库上声明合约。 - porges

你不应该像KoMet所说的那样，对于内部字段使用Requires()。 - Stephen Drew

另一种方法是创建一个SafeOfType<T>扩展方法，它确保结果不为空，然后由return source == null ? Enumerable.Empty<T> : source.OfType<T>()组成。 - Bob Vale