Code Contracts: how to suppress this "requires unproven" warning?

Question

I have a piece of code for which cccheck tells me that a Requires() is unproven and that I should add a !string.IsNullOrWhitespace(...). That condition is already checked for as I call my own extension method that I have written back in the days of .Net 3.5:

public static bool IsEmpty(this string s)
{
    if (s == null) return true;
    if (s.Length == 0) return true;
    for (int i = 0; i < s.Length; i++)
        if (!char.IsWhitespace(s[i]))
            return false;
    return true;
}

public static bool IsNotEmpty(this string s)
{
    return !IsEmpty(s);
}

My code already requires that value is IsNotEmpty:

Contract.Requires(value.IsNotEmpty(), "The parameter 'value' cannot be null or empty.");

How can I tell cccheck (and the rest of the Code Contracts framework) that IsNotEmpty() already checks for !string.IsNullOrWhitespace(...)?

Disregarding the issues I see with your implementation, I'm curious why you implemented your own version of IsNullOrWhitespace(). Perhaps this would be a good time to reconsider your approach...? — Rick Liddle, Nov 09 '11 at 21:31
Simply because it takes less keystrokes to write `value.IsEmpty()` than `string.IsNullOrWhitespace(value)`. I wrote the `IsEmpty()` extension method before `IsNullOrWhitespace` was added to `string`. `IsNullOrEmpty` wasn't enough in an earlier project. I kept the method as part of a `StringHelpers` static class full of extension methods. I still use that class in newer projects since my webhost doesn't support .Net 4. @RickLiddle What issues are you refering to? — Minustar, Nov 09 '11 at 23:30

phoog · Accepted Answer · 2011-11-09T23:59:11.263

3

Try Contract.Ensures(Contract.Result() == !string.IsNullOrWhitespace(s))

EDIT:

Yes, I realized this would cause "ensures unproven" when I posted it and I was hoping to find some time to answer more thoroughly. One (somewhat trivial) way to fix it, if you can stand throwing away your old code:

public static bool IsEmpty(this string s) 
{ 
    Contract.Ensures(Contract.Result() == string.IsNullOrWhitespace(s))
    return string.IsNullOrWhitespace(s);
} 

public static bool IsNotEmpty(this string s) 
{ 
    Contract.Ensures(Contract.Result() == !string.IsNullOrWhitespace(s))
    return !string.IsNullOrWhitespace(s);
}

edited Nov 09 '11 at 23:59

answered Nov 09 '11 at 21:35

phoog

42,068
6
79
117

This results in a “ensures unproven” instead of the previous “requires unproven”. :( Yet, on the right path, I think. – Minustar Nov 09 '11 at 23:54
A viable solution! And if I combine it with the solution given in http://stackoverflow.com/questions/3436526, I can keep my old code if I reference StringHelpers.csproj in another project written for .Net 3/3.5. – Minustar Nov 10 '11 at 00:13

Code Contracts: how to suppress this "requires unproven" warning?

1 Answers1