代码合同 - 假设与要求

Question

这两个陈述之间有什么不同？

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

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

Answer 1

想象一下,你有一个像这样的方法:

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

现在,如果传递null给它,这个方法总是会失败,所以你要确保这种方法永远不会发生.这Contract.Requires是为了什么.它为该方法设置了一个前提条件,该方法必须为true才能使方法正确运行.在这种情况下,我们将:

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

    return s.Contains("X");
}   

(注意:Requires并且Ensures必须始终位于方法的开头,因为它们是关于整个方法的信息. Assume在代码本身中使用,因为它是关于代码中该点的信息.)

现在,在调用方法"ContainsAnX"的代码中,必须确保字符串不为null.您的方法可能如下所示:

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不是null.

但是,您可能正在调用外部库,这些库没有关于它们返回的值的任何信息(即它们不使用代码约定).让我们改变一下这个例子:

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(或永远不应该!).在这种情况下,我们知道的不仅仅是静态检查器,所以我们可以告诉它Assume变量永远不会为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.

您可能需要假设的另一种情况是您的前提条件非常复杂且静态检查器很难证明它们.在这种情况下,你可以给它一点点推动,以帮助它:)

就运行时行为而言,使用Assume和Requires之间没有太大区别.但是,静态检查器的结果会有很大差异.每个人的意思也是不同的,就谁在失败时负责错误而言:

• 需要意味着调用此方法的代码 必须确保条件成立.
• 假设意味着这种方法正在做出一个应该始终成立的假设.