c# - 如何向 CodeContracts 证明 while 循环后的条件为真

Question

我正在尝试使用 CodeContracts。我从一个小功能开始

public static string MyTrim(string text)
{
    Contract.Requires(text != null);
    Contract.Ensures(Contract.Result<string>().Length == 0 || Contract.Result<string>()[0] != ' ');
    var sCurrent = text;
    while (sCurrent.Length != 0 && sCurrent[0] == ' ')
    {
        sCurrent = sCurrent.Substring(1);
    }
    return sCurrent;
}

Code Contracts 对我说我没有证明 Ensures。但是在while循环之后，我知道条件是错误的。所以我知道

Scurrent.Length == 0 || Scurrent[0] != ' '

这正是我的保证条件。我能做些什么来向代码合同解释这一点？

Answer 1

我已经研究了您的示例中发生的情况，这只是由于析取循环条件而导致的静态检查器的限制。我们会努力解决这个问题。