代码契约：确保字符串的方法得到证实(Code Contracts: Ensure unproven

我玩弄代码合同，有一个简单的方法，将各字符间的空格字符给定数。

如

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

但警告仍然存在。 哪些假设必须作出摆脱的警告？

先感谢您。

Answer 1:

从根本上说，我觉得你问太多的静态检查在这种情况下。 这将是相当可观的，如果它真的可以工作了这一点。 在这种情况下，我认为你就得忍受它作为一个执行时间检查，而不是一个编译时检查。

我不知道是否有说法的一种特定的方式“请确保这是一个后置条件，但不要试图证明这一点” -呼吁Contract.Assume 与后置条件的方法可以做到这一点的结束，但它很可能意味着评估两次:(

（顺便说一句，你的实现是目前真正的无效率的。这不是这个问题的话题，但仍是值得期待的。）

Answer 2:

我觉得你的假设是错误的。 它并不适用于S.Length == 0 ：第二ensures你会得到一个是负面的价值。

其次，这是不平凡的检查ensures在编译时声明。 也许只是没有在检查中实现..

也许你可以有不同的实现你的循环。 删除您if语句，并从0环路S.Length-2。 但我不知道..

Answer 3:

尝试这个

        public string InsertSpaceBetweenLetters(string S, int spaceWidth) {

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

        StringBuilder result = new StringBuilder(String.Empty);

        int count = 0;
        int final = S.Length - 1;
        foreach ( char c in S )
        {
            result.Append(c, 1);
            if ( count < final )
            {
                result.Append(' ', spaceWidth);
            }
            ++count;
        }
        return result.ToString();
    }

文章来源: Code Contracts: Ensure unproven on string method