我如何使用代码契约来检查Lazy<而不会失去惰性求值的优点

本文关键字:失去 代码 何使用 契约 Lazy 检查 | 更新日期: 2023-09-27 18:04:01

我的代码看起来像这样:

public class Foo
{
    private readonly Lazy<string> lazyBar;
    public Foo()
    {
        lazyBar = new Lazy<string>(() => someExpression);
    }
    public string Bar
    {
        get { return lazyBar.Value; }
    }
    public void DoSomething()
    {
        Contract.Requires(Bar != null); // This evaluates Bar, but all I really require is that WHEN Bar is evaluated, it is not null.
        ...
    }
}

现在,每一个地方调用DoSomething,我们也必须证明Bar不为空。但是检查这一点不会消除惰性求值的好处吗?另外,我们不应该在合同中避免副作用吗?

是否有可能证明someExpression不会解析为null,而不求值?

我如何使用代码契约来检查Lazy<而不会失去惰性求值的优点

Code Contracts对Lazy<T>没有足够的了解,以便在原始lambda和返回的结果之间建立联系。

你真正想要能够声明的是(对于Lazy<T>),任何包含lambda返回值的契约也包含Value的值,但是像这样的元级契约目前是不可能的。

你可以做的是将someExpression移动到一个方法中,然后将Contract.Ensures变为result != null。如果这个条件不成立,它会警告你。然后,您可以将Invariant放在结果上;lazyBar.Value != null。这将意味着它实际上不是懒惰,但对于你的发布代码,你可以在ReleaseRequires模式下使用CC构建,这些类型的检查将被消除(强烈建议阅读不同"级别"的合同执行手册!)

在你在代码中编辑了你的评论之后,我可以回答你的问题,但我不认为我在回答隐藏在阴影中的确切问题,你是法官。

如果从中读取属性解析为的唯一方法是实际从它中读取,计算构建底层Lazy<T>字段的表达式。

现在,您可以做的是检查底层字段以询问它是否已被求值。

换句话说,你可以这样做:

if (lazyBar.IsValueCreated)
    ....

现在,我不确定这是否适用于合同,但以下内容应该允许您检查:

Contract.Requires(!lazyBar.IsValueCreated || lazyBar.Value != null);

由于我不是契约方面的专家,我不知道上面的代码是否会被转换成表达式树并以任何一种方式求值。

这部分取决于您处理的类型。

例如,继承自ICollection的类型将不会在求值Count()这样的方法时被迭代。

在实现iccollection的情况下,Count()方法被优化以检查Count属性。

如果你只是想检查你的Lazy对象内部是否有"某些东西",我建议使用System.Linq命名空间中可用的Any()方法。

这将只需要在集合中执行一个MoveNext,然后才能确定其中是否有"任何"

我不明白为什么这不起作用(它确实不起作用):

公共类Foo{private readonly;

public Foo()
{
    lazyBar = new Lazy<string>(() => someExpression);
    Contract.Ensures(!lazyBar.IsValueCreated);
}
    [ContractInvariantMethod]
    private static void Invariant()
    {
        Contract.Invariant(!lazyBar.IsValueCreated || lazyBar.Value != null);
    }
public void DoSomething()
{
    Contract.Assume(lazyBar.IsValueCreated);
    lazyBar.Value.AccessSomeMethod; //Here Code Contracts detect "Possibly calling a method on a null reference"
    ...
}

}