C# Code Contracts: Why can't this simple condition be proven?

I'm doing a simple test of Code Contracts. The following code is in a winform. This passes (of course):

    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(开发者_StackOverflow中文版this);

        base.OnLoad(e);
    }

However, I add just a very simple level of indirection, it says "requires unproven":

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

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

        base.OnLoad(e);
    }

This seems like it would be trivial to prove. Why isn't it working?

Your Valid method hasn't got any contracts on it. You could express a contract there, which would probably just be the same the code, really... but Code Contracts isn't going to assume that. Your implementation could change - you haven't told Code Contracts what the method is meant to do, so it doesn't assume anything from the implementation.

Do you really need a method just to call string.IsNullOrEmpty(str)? And since String.IsNullOrEmpty(string) is already marked as [Pure] in the BCL, and since the wrapper is extraneous, the whole problem would just go away if you called it directly.

If you really feel strongly about this method, then one way this might work with your current code is to change your contract on your Test method:

private void Test(Form form)
{
    Contract.Requires(Valid(form.Name));

    MessageBox.Show(form.Name);
}

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

Now the static analyzer shouldn't complain.