代码之家 › 专栏 › 技术社区 › Damien_The_Unbeliever

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

code-contracts .net c#

2

Damien_The_Unbeliever · 技术社区 · 15 年前

我在尝试什么,对我来说,似乎是一些相当基本的代码合同代码。我把它归结为以下问题。以下消息导致静态分析失败

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; } }
    }

}

当我在界面中放置契约时,我需要做什么来满足静态检查器的要求?

1 回复 | 直到 15 年前

1

3

Rich 15 年前

在你实施 IBasic , StrippedContract Frozen 属性:

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

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