c# - while ループの後の条件が true であることを CodeContracts に証明する方法

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 ループの後、条件が false であることがわかります。だから私はそれを知っています

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

これはまさに私の確実な条件です。Code CONtracts にそれを説明するにはどうすればよいですか?

Answer 1

あなたの例で何が起こっているかを調べましたが、これは分離ループ状態による静的チェッカーの単なる制限です。これを修正しようとします。