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

Question

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(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?

Answer 1

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.