C# 代码契约(Contract) : Why can't this simple condition be proven?

Question

我正在对代码契约进行简单测试。以下代码是在 winform 中。这通过了(当然):

    private void Test(Form form)
    {
        Contract.Requires(!string.IsNullOrEmpty(form.Name));

        MessageBox.Show(form.Name);
    }

    protected override void OnLoad(EventArgs e)
    {
        if (!string.IsNullOrEmpty(Name))
            Test(this);

        base.OnLoad(e);
    }

但是，我只添加了一个非常简单的间接级别，它说“需要未经证实”:

    private bool Valid(string str)
    {
        return !string.IsNullOrEmpty(str);
    }

    protected override void OnLoad(EventArgs e)
    {
        if (Valid(Name))
            Test(this);

        base.OnLoad(e);
    }

这似乎很容易证明。为什么它不起作用？

Answer 1

您的 Valid 方法没有任何契约。您可以在那里表达契约(Contract)，这可能与代码相同，真的……但代码契约(Contract)不会假设这一点。您的实现可能会发生变化 - 您没有告诉 Code Contracts 该方法意味着要做什么，因此它不会从实现中假设任何东西。