代码契约 - 假设与要求

发布于 2024-10-13 08:33:07 字数 155 浏览 4 评论 0原文

这两种说法有什么区别？

Contract.Requires(string.IsNullOrWhiteSpace(userName));

Contract.Assume(string.IsNullOrWhiteSpace(userName));

原文

What's the diference between these two statements ?

Contract.Requires(string.IsNullOrWhiteSpace(userName));

Contract.Assume(string.IsNullOrWhiteSpace(userName));

分享到QQ

分享到微博

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

发布评论

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

岁月打碎记忆 2024-10-20 08:33:07

想象一下您有一个这样的方法：

bool ContainsAnX(string s)
{
    return s.Contains("X");
}

现在，如果您将 null 传递给该方法，该方法将始终失败，因此您希望确保这种情况永远不会发生。这就是 Contract.Requires 的用途。它为该方法设置了一个前提条件，该条件必须为真才能使该方法正确运行。在这种情况下，我们将：（

bool ContainsAnX(string s)
{
    Contract.Requires(s != null);

    return s.Contains("X");
}

注意：Requires和Ensures必须始终位于方法的开头，因为它们是有关方法作为一个整体在代码本身中使用，因为它是有关代码中该点的信息。）

现在，在调用方法“ContainsAnX”的代码中，您必须确保字符串不为空。您的方法可能如下所示：

void DoSomething()
{
    var example = "hello world";

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

这会正常工作，并且静态检查器可以证明 example 不为空。

但是，您可能会调用外部库，这些库没有有关它们返回的值的任何信息（即它们不使用代码契约）。让我们改变一下这个例子：

void DoSomething()
{
    var example = OtherLibrary.FetchString();

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

如果 OtherLibrary 不使用代码契约，静态检查器会抱怨 example 可能为空。

也许他们的库文档说该方法永远不会返回 null（或者应该永远不会！）。在这种情况下，我们比静态检查器知道更多，因此我们可以告诉它假设变量永远不会为空：

void DoSomething()
{
    var example = OtherLibrary.FetchString();

    Contract.Assume(example != null);

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

现在这对于静态检查器来说是可以的检查员。如果您启用了运行时合约，则还将在运行时检查假设。

您可能需要假设的另一种情况是当您的先决条件非常复杂并且静态检查器很难证明它们时。在这种情况下，您可以稍微推动它以帮助它前进:)

就运行时行为而言，使用 Assume 和 Requires 之间不会有太大区别。然而，静态检查器的结果会有很大差异。每个的含义也不同，就失败时谁对错误负责而言：

Requires 表示调用此方法的代码必须确保条件成立。
假设意味着此方法正在做出一个应该始终成立的假设。

Imagine you have a method like this:

bool ContainsAnX(string s)
{
    return s.Contains("X");
}

Now, this method will always fail if you pass null to it, so you want to ensure this never happens. This is what Contract.Requires is for. It sets a precondition for the method, which must be true in order for the method to run correctly. In this case we would have:

bool ContainsAnX(string s)
{
    Contract.Requires(s != null);

    return s.Contains("X");
}

(Note: Requires and Ensures must always be at the start of a method, as they are information about the method as a whole. Assume is used in the code itself, as it is information about that point in the code.)

Now, in your code that calls the method "ContainsAnX", you must ensure that the string is not null. Your method might look like this:

void DoSomething()
{
    var example = "hello world";

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

This will work fine, and the static checker can prove that example is not null.

However, you might be calling into external libraries, which don't have any information about the values they return (i.e. they don't use Code Contracts). Let's change the example:

void DoSomething()
{
    var example = OtherLibrary.FetchString();

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

If the OtherLibrary doesn't use Code Contracts, the static checker will complain that example might be null.

Maybe their documentation for the library says that the method will never return null (or should never!). In this case, we know more than the static checker does, so we can tell it to Assume that the variable will never be null:

void DoSomething()
{
    var example = OtherLibrary.FetchString();

    Contract.Assume(example != null);

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

Now this will be okay with the static checker. If you have runtime contracts enabled, the Assume will also be checked at run time.

Another case where you might need Assume is when your preconditions are very complex and the static checker is having a hard time proving them. In this case you can give it a bit of a nudge to help it along :)

In terms of runtime behavior there won't be much difference between using Assume and Requires. However, results with the static checker will differ greatly. The meaning of each is different as well, in terms of who is responsible for the error in case of failure:

Requires means that the code which calls this method must ensure the condition holds.
Assume means that this method is making an assumption which should always hold true.

回复收藏 0 原文