c# - コード コントラクト: 文字列メソッドで証明されていないことを確認する

Question

私はコード契約をいじっていて、各文字の間に指定された数のスペース文字を挿入する簡単な方法を得ました。

例えば

Hello -> H e l l o
World -> W   o   r   l   d

メソッド InsertSpaceBetweenLetters は、文字列プロパティ S (変更後に返される文字列) を提供するクラス内で実装されます。これがコードです

public string InsertSpaceBetweenLetters(int spaceWidth)
{
    Contract.Requires(spaceWidth > 0);
    Contract.Requires(S.Length > 0);
    Contract.Ensures(Contract.Result<string>() != null);
    Contract.Ensures(Contract.Result<string>().Length == S.Length + (S.Length - 1) * spaceWidth);

    string result = String.Empty;

    Contract.Assume(S.Length >= 0);
    for(int i = 0; i < S.Length; i++)
    {
        result += S[i];
        if (i < S.Length - 1)
            result += new String(' ', spaceWidth);
    }
    return result;
}

静的チェッカーは、次の警告を表示します。

ensures unproven: Contract.Result<string>().Length == S.Length + (S.Length - 1) * spaceWidth

ループの前に行っている仮定で、この警告を取り除くことができると思いました:

Contract.Assume(S.Length >= 0);

しかし、警告はまだ残っています。警告を取り除くには、どのような仮定を立てる必要がありますか?

前もって感謝します。