实现接口时，通过属性确保未经证实

我正在尝试对我来说，似乎是一些相当基本的代码合同代码。 我把它减少到了下面的问题。 以下内容未通过消息进行静态分析

CodeContracts：确保未经证实：this.Frozen

using System; using System.Diagnostics.Contracts; namespace PlayAreaCollection2010 { public class StrippedContract : IBasic { private bool _frozen = false; public void Freeze() { _frozen = true; } public bool Frozen { get { return _frozen; } } } [ContractClass(typeof(IBasicContract))] public interface IBasic { void Freeze(); bool Frozen { get; } } [ContractClassFor(typeof(IBasic))] public abstract class IBasicContract : IBasic { #region IBasic Members public void Freeze() { Contract.Ensures(this.Frozen); } public bool Frozen { get { return true;} } #endregion } } 

但是，以下工作正常并满足所有检查：

 using System; using System.Diagnostics.Contracts; namespace PlayAreaCollection2010 { public class StrippedContract { private bool _frozen = false; public void Freeze() { Contract.Ensures(this.Frozen); _frozen = true; } public bool Frozen { get { return _frozen; } } } } 

CodeContracts：检查1断言：1正确

当我将合同放入界面时，我需要做些什么来满足静态检查器？

Answer 1

在您的IBasic ， StrippedContract实现中，您需要向Frozen属性添加一个后置条件：

 public bool Frozen { get { Contract.Ensures(Contract.Result() == this._frozen); return _frozen; } } 

或者，您可以在项目属性的“代码约定”选项卡中将-infer命令行选项添加到静态检查器。 这将允许静态检查器自动推断它。