代码合同是否未能发现Nullable<T>.HasValue和null之间明显的关系？

Question

代码合同是否未能发现Nullable<T>.HasValue和null之间明显的关系？

11

我正在尝试将代码合约应用到我的代码中，但我遇到了一个令人困惑的问题。这段代码未能满足合约，但除非我真的很愚蠢，否则我希望它能够轻松地分析出在返回点上id必须有一个值。

if (id == null)
    throw new InvalidOperationException(string.Format("{0} '{1}' does not yet have an identity", typeof(T).Name, entity));

return id.Value;

Code Contracts error: requires unproven: HasValue

- Wheelie

你尝试过 !id.HasValue 吗？ - Daniel A. White

3

“id”字段的定义是什么？它是否是“readonly”（只读）的？ - Sven

1

非常准确，Sven！不错的心理调试技巧 :)（见下文） - Wheelie

3个回答

1

你可以尝试将字段复制到本地变量中，并使用该本地变量编写语句。证明器可能会对字段保守，因为调用可能会改变字段值。

- Dan Bryant

根据发现的问题，我相信这个方法会起作用。通过显式创建副本，它只会创建一次副本，而不是两次（如隐式只读情况下）。 - Dan Bryant

0

它没有将你的 if throw 检查视为其合同的一部分。请尝试使用以下代码：

if (id == null)    
  throw new InvalidOperationException(string.Format("{0} '{1}' does not yet have an identity", typeof(T).Name, entity));

Contract.EndContractBlock();

http://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.contract.endcontractblock.aspx

- Andy

这是我最初的想法，但是 'id' 在这里是一个字段，因此可能不适合添加要求（代码的客户端可能无法直接确保要求能够满足）。如果 'id' 应该始终被设置，那么将其作为类不变量可能是有意义的，但否则它只是一个状态检查，不应该有调用者要求。 - Dan Bryant

事实上，您的if then throw实际上是一个合同，无论您的客户是否能够影响检查结果。添加EndContractBlock唯一的作用是让CC意识到您的if then throw是一个合同，而它目前并不知道。 - Andy

这是正确的。将此状态检查封装在可见属性中可能是一个好的提示，以便客户端可以直接知道是否已经履行了合同，将对象放置在正确的状态进行调用。 - Dan Bryant

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Wheelie · Accepted Answer

我已经了解了这个行为，这不是Code Contract的问题。

我在ILSpy中打开了生成的程序集，这就是生成的代码：

public Guid Id
{
    get
    {
        Guid? guid = this.id;
        if (!guid.HasValue)
        {
            throw new InvalidOperationException();
        }
        guid = this.id;
        return guid.Value;
    }
}

实例变量id被复制到一个本地变量中，而这个本地变量在条件块后被重置回其原始值。现在显然为什么代码合同显示合同违规错误，但它仍然让我困惑的是为什么代码被以这种形式重写。我进行了更多的实验，并完全将代码合同从项目中删除，很明显这是标准的C#编译器行为，但为什么呢？

秘密似乎是由于一个小细节，我意外地省略了我的原始问题。id实例变量声明为readonly，这似乎是导致编译器添加临时guid变量的原因。

我必须承认我仍然困惑为什么编译器觉得需要这样做来确保id的不可变性保证，但我会继续深入研究...