c# – 代码合同：如何在财产获取方面满足’确保未经证实’？

发布时间：2020-12-15 17:28:02 所属栏目：百科来源：网络整理

导读：我有以下界面： [ContractClass(typeof(MyObjectContract))]public interface IMyObject{ int CountOfItems { get; }} 以下合同： [ContractClassFor(typeof(IMyObject))]public abstract class MyObjectContract{ int IMyObject.CountOfItems { get { Contr

我有以下界面：

[ContractClass(typeof(MyObjectContract))]
public interface IMyObject
{
    int CountOfItems { get; }
}

以下合同：

[ContractClassFor(typeof(IMyObject))]
public abstract class MyObjectContract
{
    int IMyObject.CountOfItems
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() > 0);
            return 1;
        }
    }
}

以下实施：

public class MyObject : IMyObject
{
    private IEnumerable someEnumerable .... 

    public int CountOfItems
    {
        get
        {
            return this.someEnumerable.Count();
        }
    }
}

现在我收到警告说确保未经证实：Contract.Result< int>()> 0

我怎么能证明计数大于零？我不想在getter中抛出异常,我错过了什么？

谢谢

解决方法

正如其他人所提到的,由于基类库(.NET Framework)和静态检查器的限制,您无法静态证明IEnumerable< T> .Count()返回大于0的值.但是,您可以向静态检查器指示您认为该事实为真.这是您使用基类库解决所有此类合同问题的方法,或静态检查程序无法证明的语句.

public int CountOfItems
{
    get
    {
        int count = this.someEnumerable.Count();
        Contract.Assume(count > 0);
        return count;
    }
}

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!