0

我正在玩代码合同，并得到了一个简单的方法，在每个字符之间插入给定数量的空格字符。

例如

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

但警告仍然存在。必须做出哪些假设才能消除警告？

先感谢您。

4

3 回答 3

3

从根本上说，我认为在这种情况下你对静态检查器的要求太多了。如果它真的能解决这个问题，那将是非常令人印象深刻的。在这种情况下，我认为您只需要忍受它是执行时检查而不是编译时检查。

我不知道是否有一种特定的方式说“请确保这是一个后置条件，但不要试图证明它” -在方法末尾Contract.Assume 使用后置条件调用可能会这样做，但它可能意味着对其进行两次评估:(

（顺便说一句，您的实现目前确实效率低下。这不是这个问题的主题，但仍然值得一看。）

于 2012-11-21T11:03:27.833 回答
1

我认为你的假设是错误的。它不适用于S.Length == 0: 在第二个ensures你会得到一个负值。

其次，检查ensures编译时的语句并非易事。可能只是没有在检查器中实现..

也许你可以以不同的方式实现你的循环。删除您的if语句并从 0 循环到 S.Length-2。但我不确定..

于 2012-11-21T11:05:24.130 回答
0

试试这个

        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();
    }
于 2013-12-26T00:57:33.083 回答