代码契约迭代器中的错误？

发布于 2024-07-26 03:25:34 字数 372 浏览 11 评论 0 原文

以下代码在前提条件下失败。这是代码合约中的错误吗？

static class Program
{
    static void Main()
    {
        foreach (var s in Test(3))
        {
            Console.WriteLine(s);
        }
    }

    static IEnumerable<int>Test (int i)
    {
        Contract.Requires(i > 0);
        for (int j = 0; j < i; j++)
            yield return j;
    }
}

原文

The following code fails on the pre condition. Is this a bug in code contracts?

static class Program
{
    static void Main()
    {
        foreach (var s in Test(3))
        {
            Console.WriteLine(s);
        }
    }

    static IEnumerable<int>Test (int i)
    {
        Contract.Requires(i > 0);
        for (int j = 0; j < i; j++)
            yield return j;
    }
}

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

寂寞清仓 2024-08-02 03:25:35

这是博客文章与这个主题相关，涉及单元测试、迭代器、延迟执行和您。

延迟执行就是这里的问题。

回复收藏 0 原文

深海不蓝 2024-08-02 03:25:35

此代码将与 .NET 4.0 的最终版本（刚刚尝试过）一起使用，其中支持交互器中的代码契约，但正如我最近发现的那样，它并不总是能正常工作（了解更多此处）。

回复收藏 0 原文

嘿嘿嘿 2024-08-02 03:25:35

这可能是过去 CodeContract 重写器中的一个问题。但当前版本似乎在您的示例中表现良好。这里不存在迭代器/延迟评估等问题。参数 i 由值捕获，并且在迭代期间不会改变。合约应该仅在调用 Test 开始时检查这一点，而不是在每次迭代期间检查。

回复收藏 0 原文

拥抱影子 2024-08-02 03:25:34

我的猜测是这与迭代器的延迟性质有关。请记住，合同处理将发生在最终发出的 IL 上，而不是 C# 代码上。这意味着您必须考虑迭代器和 lambda 表达式等功能的生成代码。

如果你反编译该代码，你会发现“i”实际上并不是一个参数。它将是类中用于实现迭代器的变量。所以代码实际上看起来更像下面这样，

class IteratorImpl {
  private int i;
  public bool MoveNext() {
    Contract.Require(i >0);
    ..
  }
}

我对合约 API 不太熟悉，但我的猜测是生成的代码更难验证。

My guess is this has to do with the delayed nature of iterators. Remember, contract processing will occur on the final emitted IL, not the C# code. This means you have to consider the generated code for features like iterators and lambda expressions.

If you decompile that code you'll find that "i" is not actually a parameter. It will be a variable in the class which is used to implement the iterator. So the code actually looks more like the following

class IteratorImpl {
  private int i;
  public bool MoveNext() {
    Contract.Require(i >0);
    ..
  }
}

I'm not terribly familiar with the contract API but my guess is the generated code is much harder to verify.

回复收藏 0 原文

救星 2024-08-02 03:25:34

请记住，迭代器在枚举之前不会运行，并在后端编译成一些特殊的酱汁。如果你想验证参数，你应该遵循的一般模式（这可能适用于合约）是有一个包装函数：

static IEnumerable<int> Test (int i)
{
    Contract.Requires(i > 0);
    return _Test(i);
}

private static IEnumerable<int> _Test (int i)
{
    for (int j = 0; j < i; j++)
        yield return j;
}

这样 Test() 将在调用时检查参数，然后返回 _Test()，它实际上只是返回一个新类。

Remember that iterators aren't run until they are enumerated, and are compiled into some special sauce in the back end. The general pattern you should follow if you want to validate parameters, and this probably holds true for contracts, is to have a wrapper function:

static IEnumerable<int> Test (int i)
{
    Contract.Requires(i > 0);
    return _Test(i);
}

private static IEnumerable<int> _Test (int i)
{
    for (int j = 0; j < i; j++)
        yield return j;
}

That way Test() will do the checking of the parameters when it is called then return _Test(), which actually just returns a new class.

回复收藏 0 原文

~没有更多了~