c# - 代码合约编译器怎么会认为这可能是空的？

Question

我遇到了多个似乎是一种模式的案例：

Contract.Ensures(Contract.Result<BlahType>() != null);
...
BlahType Blah = new BlahType();
...
...
return Blah;

它抱怨。

在所有情况下，该字段都是私有的，并且该方法中的其他任何内容都不会与它混淆。（这些都是惰性初始化，因为数据必须来自磁盘。）

当然我可以在这里添加一个 Contract.Assume 但我不喜欢那种答案。

Answer 1

让静态检查器相信字段永远不会null（或任何其他条件）的唯一方法是使其成为不变量。不变量方法中的不变量在您的类中每个方法的返回时被检查，因此检查器可能假设它们成立。因此，添加到类的底部：

#region Invariants
[ContractInvariantMethod]
[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Performance",
    "CA1822:MarkMembersAsStatic",
    Justification = "Required for code contracts.")]
private void ObjectInvariant()
{
    Contract.Invariant(this.blah != null);
}
#endregion

笔记：

• 不变方法是任何private void没有参数但ContractInvariantMethod应用了属性的方法。您可以在其中放置多个不变量。
• 要快速获取ObjectInvariant方法片段，请键入cimTABTAB。
• 可以在此处找到其他代码合同片段。
• 在 C# 中，私有/受保护字段和局部变量用小写的标识符的第一个字母（驼峰式）编写。请参阅此处了解更多信息。这使您的代码更具可读性和可理解性。