未验证确保在接口的组合中引用另一个属性

本文关键字：引用 另一个 属性 组合 验证 确保 接口 | 更新日期: 2023-09-27 18:01:24

假设代码如下:

[ContractClass(typeof(ICC4Contract))]
public interface ICC4
{
    bool IsFooSet { get; }
    string Foo { get; }
}
public class CC4 : ICC4
{
    private string _foo;
    public bool IsFooSet { get { return Foo != null; } }
    public string Foo { get { return _foo; } }
}
[ContractClassFor(typeof(ICC4))]
public abstract class ICC4Contract : ICC4
{
    public bool IsFooSet
    {
        get
        {
            Contract.Ensures((Contract.Result<bool>() && Foo != null)
                             || !Contract.Result<bool>());
            return false;
        }
    }
    public string Foo
    {
        get
        {
            Contract.Ensures((Contract.Result<string>() != null && IsFooSet)
                             || !IsFooSet);
            return null;
        }
    }
}

合同试图说:

  1. 如果Foo不是null, IsFooSet将返回true。
  2. 如果IsFooSet返回true, Foo不返回null。

这几乎可以工作。
然而，我在return _foo;上得到了一个"未证实的保证"，因为检查器没有意识到Foo总是等于_foo。

将Foo更改为带有private setter的自动属性会删除该警告，但我不想这样做(我不喜欢带有私有setter的自动属性)。

我必须在上述代码中更改什么以使警告消失，同时保留_foo字段?

下面的代码不能用:

  1. 将IsFooSet改为使用_foo而不是Foo。这将导致IsFooSet上额外的"确保未经证实"。
  2. 添加不变量Foo == _foo。这将导致隐式默认构造函数出现"未验证的不变"。此外，在真实的代码库中，静态检查器的处理时间要高得多。
  3. 根据这个答案将Contract.Ensures(Contract.Result<string>() == _foo);添加到Foo的getter中不会改变任何东西。

未验证确保在接口的组合中引用另一个属性

您可以使用短路来简化条件，并且出于某种原因，这是有效的:

[ContractClassFor(typeof(ICC4))]
public abstract class ICC4Contract : ICC4
{
    public bool IsFooSet
    {
        get
        {
            Contract.Ensures(!Contract.Result<bool>() || Foo != null);
            return false;
        }
    }
    public string Foo
    {
        get
        {
            Contract.Ensures(!IsFooSet || Contract.Result<string>() != null);
            return null;
        }
    }
}
相关文章：