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

Question

我正在尝试对我来说似乎是一些相当基本的代码合约代码。我已将其简化为以下问题。以下静态分析失败，并显示消息

CodeContracts：确保未经证实： 这个.冻结

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<bool>() == this._frozen);
        return _frozen;
    }
}

或者，您可以添加 < code>-infer 命令行选项添加到项目属性的“代码合同”选项卡中的静态检查器。这将允许静态检查器自动推断这一点。