Code Contracts: Ensure unproven on string method

Question

I'm playing around with code contracts and got a simple method inserting a given count of space characters between each character.

e.g.

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

The method InsertSpaceBetweenLetters is implemented within a class that offers some string-property S, the string that should be returned after modification. Here's the code

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

The static checker gives me the following warning:

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

I thought I could get rid of this warning with the assumption I'm doing before the loop:

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

But the warning is still there. What assumptions have to be made to get rid of the warning?

Thank you in advance.

Answer 1

I think your assumption is wrong. It doesn't hold for S.Length == 0: in the second ensures you would get a negativ value.

Second, it's not trivial to check your ensures statement on compile time. Probably just not implemented in the checker..

Maybe you could implement your loop differently. Remove your if statement and loop from 0 to S.Length-2. But I'm not sure..

Answer 2

Fundamentally, I think you're asking too much of the static checker in this case. It would be pretty impressive if it really could work that out. In this case I think you'll just have to live with it being an execution-time check rather than a compile-time check.

I don't know if there's a specific way of saying "please ensure this as a post-condition, but don't try to prove it" - calling Contract.Assume with the post-condition at the end of the method may do it, but it would probably mean evaluating it twice :(

(As an aside, your implementation is currently really inefficient. That's not the topic of this question, but is still worth looking at.)

Answer 3

Try this

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