有没有办法让代码合同与 LINQ 一起工作？答案

【问题标题】：Is there any way to make Code Contracts work with LINQ?有没有办法让代码合同与 LINQ 一起工作？
【发布时间】：2023-03-28 22:05:01
【问题描述】：

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

    public IEnumerable<string> GetCarModelsByMake(string make)
    {
        return from car in Cars
               where car.Make == make
               select car.Model;
    }

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

    public IEnumerable<string> GetCarModelsByMake(string make)
    {
        Contract.Assume(Cars.All(car => car != null));

        return from car in Cars
               where car.Make == make
               select car.Model;
    }

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

    [SuppressMessage("Microsoft.Contracts", "NonNull")]

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

    [SuppressMessage("Microsoft.Contracts", "Requires")]
    [SuppressMessage("Microsoft.Contracts", "Ensures")]
    [SuppressMessage("Microsoft.Contracts", "Invariant")]

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

    [ContractVerification(false)]

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

    public IEnumerable<string> GetCarModelsByMake(string make)
    {
        return from car in Cars
               where car != null && car.Make == make
               select car.Model;
    }

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

    public IEnumerable<string> GetCarModelsByMake(string make)
    {
        return from car in Cars
               where car != null && car.Make == make
               select car == null ? null : car.Model;
    }

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

【问题讨论】：

标签： c# .net linq code-contracts

【解决方案1】：

它可能会抱怨对 Cars 进行 null 检查。试试这个：

公共 IEnumerable GetCarModelsByMake（字符串制作） { 如果（空==汽车）返回新字符串[0]； // 或者如果你喜欢 null 从汽车返回哪里 car.Make == 制作选择汽车。型号； }

请记住，此 LINQ 语句实际上与以下内容相同：

return Cars.Where(car => car.Make == make).Select(car => car.Model);

如果 Cars 为空，你会得到一个异常。

【讨论】：

+1 但我认为将Cars != null 添加到类不变量将更接近原始代码的精神，这显然不希望Cars 成为null。 msdn.microsoft.com/en-us/magazine/ee236408.aspx#id0070066
绝对的；此类的不变量将更适合此问题的代码合同性质。
我应该澄清一下，该类已经有一个保证 Cars != null 的不变量。但这不是合同警告的内容。警告是关于“汽车”变量为空，而不是“汽车”集合。
您能否添加另一个不变量，例如“!Cars.Contains(null)”？

【解决方案2】：

您是否尝试过最新版本的代码合同？有一个在 10 月发布，我无法用它来复制它。

另外，代码协定在静态 Contracts 类上定义了自己的 ForAll 方法，它的逻辑可能比 LINQ 扩展 All 方法更好。

【讨论】：