代码合约：如何抑制这种“需要未经证实”的情况警告？

Question

我有一段代码，cccheck 告诉我 Requires() 未经验证，我应该添加 !string.IsNullOrWhitespace(...)。当我调用我自己在 .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);
}

我的代码已经要求 value 为 IsNotEmpty：

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

如何我可以告诉 cccheck （以及代码契约框架的其余部分）IsNotEmpty() 已经检查 !string.IsNullOrWhitespace(...)？

Answer 1

尝试 Contract.Ensures(Contract.Result() == !string.IsNullOrWhitespace(s))

编辑：

是的，我意识到这会导致“确保未经证实”，当我发布它时，我希望找到有时间更彻底地回答。如果您可以忍受扔掉旧代码，则可以使用一种（有点微不足道的）方法来修复它：

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);
}