c# - 在实现接口(interface)时通过属性确保未经证实

Question

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

CodeContracts: ensures unproven: 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: Checked 1 assertion: 1 correct

当我将合约放入界面后，我需要做什么来满足静态检查器的要求？

Answer 1

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

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

或者，您可以将 -infer 命令行选项添加到项目属性的代码契约(Contract)选项卡中的静态检查器。这将允许静态检查器自动推断这一点。