c# - 在 Func<> 上定义代码契约

Question

我正在尝试整合 Code Contracts到一些现有的代码中，到目前为止，大部分都很好。我面临的问题是，我已经在一个接口(interface)上设置了契约，并且一个实现将实现委托(delegate)给一个 Func<> ，它被传递到类的构造函数中，类似于以下内容:

[ContractClass(typeof(IFooContract))]
public interface IFoo
{
    object Bar();
}

[ContractClassFor(typeof(IFoo))]
public abstract class IFooContract : IFoo
{
    object IFoo.Bar()
    {
        Contract.Ensures(Contract.Result<object>() != null);
        throw new NotImplementedException();
    }
}

public class DelegatedFoo : IFoo
{
    public DelegatedFoo(Func<object> barImplementation)
    {
        Contract.Requires(barImplementation != null);
        _barImplementation = barImplementation;
    }
    private readonly Func<object> _barImplementation;

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(_barImplementation != null);
    }

    public object Bar()
    {
        //"ensures unproven: Contract.Result<object>() != null" here.
        return _barImplementation();
    }
}

静态分析器报告错误“ensures unproven: Contract.Result() != null”。我可以在 Func<> 上定义契约吗(以及在 Action<> 上的扩展)？

这是最好的解决方案吗？

public class DelegatedFoo : IFoo
{
    public DelegatedFoo(Func<object> barImplementation)
    {
        Contract.Requires(barImplementation != null);
        _barImplementation = barImplementation;
    }
    private readonly Func<object> _barImplementation;

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(_barImplementation != null);
    }

    public object Bar()
    {
        var result = _barImplementation();
        Contract.Assume(result != null);
        return result;
    }
}

Answer 1

那么，您总是可以控制Func<object>吗？实例传入？如果是这样，Func<object> 引用的每个函数参数需要有一个 Contract.Ensures(Contract.Result<object>() != null)定义后置条件。

如果你有一个 Action 也是一样的。参数，而不是。

此外，我绝对不会使用 Contract.Assume(result != null) .你确定你永远不会返回 null 吗？如果你这样做会发生什么？尝试将其更改为 Contract.Assert(result != null)反而。如果您可以控制 Func<object>参数并使用后置条件，那么您还应该能够在 public object Bar() 上指定后置条件方法并放弃对任何断言或假设的需要。

最后，您可能需要考虑添加 Contract.Ensures(_barImplementation == barImplementation)给你的 DelegatedFoo 的构造函数，不过，我想后置条件包含在定义的不变量中。我总是喜欢直截了当——这肯定不会有什么坏处，尤其是在涉及静态分析器的地方。