c# - 未经证实 确保结合接口引用另一个属性

Question

假设以下代码：

[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. IsFooSettrue如果Foo不是，将返回null。
2. Foonull如果IsFooSet返回则不返回true。

这几乎可以工作。
但是，我在 上得到一个“确保未经证实” return _foo;，因为检查员没有意识到这Foo将始终等于_foo。

使用设置器更改Foo为自动属性private会删除该警告，但我不想这样做（我不喜欢使用私有设置器的自动属性）。

_foo在保留字段的同时，我必须在上面的代码中进行哪些更改才能使警告消失？

以下不起作用：

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

Answer 1

您可以使用短路来简化条件，这出于某种原因：

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