0 <= x && s != null && x <= s.length() && count(s.substring(0, x), c) == n
How to Loop Invariant
Loop Invariants are one of the most complicated written exercises and often cause much confusion as to how they work and how to come up with a valid loop invariant.
A loop invariant must satisfy the precondition. It must thus be satisfied before the loop has been executed.
The loop invariant must hold at the beginning an after the execution of the statement in the loop body. During the execution of the loop body the invariant may not be satisfied.
The loop invariant must imply the postcondition in combination with the termination condition of the loop.
How to Construct a Loop Invariant
1 / Loop Termination Condition
Add the loop termination condition to the loop invariant but adapt it such that it is still satisfied when the loop is executed, e.g. if it is x < n then you should use x <= n.
2 / Combine Postcondition and Loop Body
Adapt the postcondition such that an adapted version of it holds after every loop body execution (and before the first) and when the loop has been executed this adapted postcondition is the postcondition itself.
3 / Add any conditions due to used methods
When you use any method inside of your loop invariant or when the code itself does operations / uses method we must makes sure that no error or exception occurs. We hence add conditions on variables to assure this is given. This includes making sure that variables are not null or arrays are non-empty.