代码契约：需要未经证实的来源！= null

Question

在阅读了对此类问题的其他一些回答后，我仍然留下警告。在此代码片段中，我从数据库中提取了 UserActivation。至此，总会至少有一个 UserActivation。如果有不止一个东西已经变成了梨形......我按照其他一些说明如何压制有关未经证实的来源的警告，但无济于事。警告是：警告 83 CodeContracts：需要未经证实：来源！= null第161行，具体行见下面的方法。

这是方法

    private static UserActivation GetUserActivation(Guid userId)
    {
        UserActivations userActivations = UserActivation.GetUserActivationsByUser(userId: userId);

        Contract.Assume(userActivations != null);

        if (userActivations.Count() > 1) // Line Number 161
            throw new Exception("More then one user action found in database");

        return userActivations[0];
    }

我使用的是 CC 版本 1.4.40602.0，此处要求的是 UserActivations 声明。

public class UserActivations : BusinessListBase<UserActivation>
{
    #region Constructors
    internal UserActivations()
    {
    }

    internal UserActivations(IList<UserActivation> list)
        : base(list)
    {
    }

    internal UserActivations(IEnumerable<UserActivation> list)
        : base(list)
    {
    }

这是 GetUserActivationByUser 方法

    public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid())
    {
        Contract.Requires(user != null || userId != null, "Either user or userId must have a value");
        Contract.Ensures(Contract.Result<UserActivations>() != null);

        Guid id = new Guid();
        if (user != null)
            id = user.Id;
        else
            id = userId;

        return new UserActivations(StorageManager.SelectAll(
            Criteria.And(
            Criteria.EqualTo("UserId", id),
            Criteria.EqualTo("Deleted", false))));
    }

原始代码是：

Public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid())
    {
        Guid id = new Guid();
        if (user != null)
            id = user.Id;
        else
            if (userId != Guid.Empty)
                id = userId;
            else
                throw new Exception("Either user or userId must have a value");

        UserActivations uas = new UserActivations(StorageManager.SelectAll(
            Criteria.And(
            Criteria.EqualTo("UserId", id),
            Criteria.EqualTo("Deleted", false))));

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

        return uas;
    }

Answer 1

我会尝试使用不同的方法，也许避免使用 linq Enumerable 扩展方法。 UserActivations 类没有自己的一些方法或属性来确定实例拥有多少个元素吗？

无论如何，您都不应该使用 Count() 扩展方法来测试序列是否为空，因为它将枚举整个序列（如果该序列未实现 ICollection代码>）。或者，正如 Pavel Gatilov 指出的那样，如果对象实现了 IQueryable，Count 可能会意外执行数据库查询。

在这里，这不是什么大问题，您期望只有一个元素，但在序列可能通常包含数千个元素的情况下，这可能是一个大问题。相反，您应该使用 Any() 扩展方法。

不过，由于从合约分析器的角度来看，使用 Any() 可能不会改变事情，因此您应该使用 UserActivations 类的 Count 属性（假设它实现了 ICollection，例如例子）。

也许您可以通过这种方式帮助合同分析器：

private static UserActivation GetUserActivation(Guid userId) 
{ 
    UserActivations userActivations = UserActivation.GetUserActivationsByUser(userId: userId); 

    IEnumerable<UserActivation> e = (IEnumerable<UserActivation>)userActivations;

    Contract.Assume(e != null); 

    if (e.Count() > 1) // Line Number 161 
        throw new Exception("More then one user action found in database"); 

    return userActivations[0]; 
} 

如果您控制 UserActivations 类，更好的解决方案是将 Contract.Ensures 添加到 GetUserActivationsByUser > 表示该方法永远不会返回 null。

Answer 2

检查您的构建日志。您错误地使用了 Contract.Ensures。您应该收到有关错误使用的警告，如下所示：

警告 CC1025：CodeContracts：在合约块之后，发现使用了合约块中定义的局部变量“dataEvents”

您的方法应该是：

public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid())
{
    Contract.Ensures(Contract.Result<UserActivations>() != null);

    Guid id = new Guid();
    if (user != null)
        id = user.Id;
    else
        if (userId != Guid.Empty)
            id = userId;
        else
            throw new Exception("Either user or userId must have a value");

    UserActivations uas = new UserActivations(StorageManager.SelectAll(
        Criteria.And(
        Criteria.EqualTo("UserId", id),
        Criteria.EqualTo("Deleted", false))));

    return uas;
}

我无法证明，但我想这可能会让验证者生气。

事实上，如果我打开运行时检查，您的代码甚至无法编译：ccrewrite 将失败。