Static checker does not understand that string is immutable

Question

 

 

public void MethodA(string input)
{
  Contract.Requires(input != null);
  string extended = input + ' ';
  Contract.Assume(extended[extended.Length - 1] == ' '); // warning : CodeContracts: requires unproven: 0 <= index
  MethodB(extended);
  Contract.Assert(extended.Length > 0);
  Contract.Assert(extended[extended.Length - 1] == ' '); // warning : CodeContracts: assert unproven
}
public void MethodB(string input)
{
  Contract.Requires(input != null);
  Contract.Requires(input.Length > 0);
  Contract.Requires(input[input.Length - 1] == ' ');
  ////Contract.Ensures(input[input.Length - 1] == ' '); // this line can prove the assert in MethodA ?!?
}

I believe the first warning may be due to a missing postcondition on string operator +(string, char).

Converting that first Assume into an Assert makes the Assert unproven. I'm not sure about that one...

But the second warning should not be there. In fact, if you add the postcondition in MethodB, that Assert is considered proven !?! 

Answer 1

The static checker currently does not reason about the content of strings. so this explains the second warning.

As for the first, this seems to be a problem with the contract on concat.

Thanks for reporting these.

---

Cheers, -MaF (Manuel Fahndrich)

Answer 2

Manuel,

Sure, there may be a problem with the contract on Concat. But notice the warning: it's about the indexer, or rather the combination of the indexer and the Length property.