Contract.Ensures 如何运作？

发布于 2024-11-29 05:11:18 字数 330 浏览 2 评论 0原文

我开始使用代码契约，虽然 Contract.Requires 非常简单，但我很难了解 Ensures 的实际作用。

我尝试创建一个像这样的简单方法：

static void Main()
{
    DoSomething();
}

private static void DoSomething() 
{
    Contract.Ensures(false, "wrong");
    Console.WriteLine("Something");
}

但我从未看到“错误”消息，也不会抛出异常或其他任何内容。

那么它实际上有什么作用呢？

原文

I'm starting to use Code Contracts, and whilst Contract.Requires is pretty straight forward, I'm having trouble seeing what Ensures actually does.

I've tried creating a simple method like this:

static void Main()
{
    DoSomething();
}

private static void DoSomething() 
{
    Contract.Ensures(false, "wrong");
    Console.WriteLine("Something");
}

I never see the message "wrong" though, nor does it throw exceptions or anything else.

So what does it actually do ?

分享到QQ

分享到微博

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

发布评论

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

凑诗 2024-12-06 05:11:18

奇怪的是它没有抛出任何东西 - 如果您正在使用适当的设置运行重写器工具。我的猜测是您正在以不检查后置条件的模式运行。

Contract.Ensures 令人困惑的地方是，您在方法的开头编写它，但它在方法的末尾执行。重写器会执行所有操作以确保其正确执行，并在必要时给出返回值。

与有关代码契约的许多事情一样，我认为最好在重写器工具的结果上运行 Reflector。确保设置正确，然后弄清楚重写器做了什么。

编辑：我意识到我还没有表达 Contact.Ensures 的观点。简而言之，它是为了确保您的方法最终完成了某些操作 - 例如，它可以确保它已将某些内容添加到列表中，或者（更有可能）返回值非空，或者正值等等。例如，您可能会：

public int IncrementByRandomAmount(int input)
{
    // We can't do anything if we're given int.MaxValue
    Contract.Requires(input < int.MaxValue);
    Contract.Ensures(Contract.Result<int>() > input);

    // Do stuff here to compute output
    return output;
}

在重写的代码中，在返回点将进行检查，以确保返回值确实大于输入。

It's odd for it to not throw anything - if you're running the rewriter tool with the appropriate settings. My guess is that you're running in a mode which doesn't check postconditions.

The confusing thing about Contract.Ensures is that you write it at the start of the method, but it executes at the end of the method. The rewriter does all the magic to make sure it executes appropriately, and is given the return value if necessary.

Like many things about Code Contracts, I think it's best to run Reflector on the results of the rewriter tool. Make sure you've got the settings right, then work out what the rewriter has done.

EDIT: I realise I haven't expressed the point of Contact.Ensures yet. Simply put, it's to ensure that your method has done something by the end - for example, it could ensure that it's added something to a list, or (more likely) that the return value is non-null, or positive or whatever. For example, you might have:

public int IncrementByRandomAmount(int input)
{
    // We can't do anything if we're given int.MaxValue
    Contract.Requires(input < int.MaxValue);
    Contract.Ensures(Contract.Result<int>() > input);

    // Do stuff here to compute output
    return output;
}

In the rewritten code, there will be a check at the point of return to ensure that the returned value really is greater than the input.

回复收藏 0 原文

~没有更多了~