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.

Three Aspects

Precondition

A loop invariant must satisfy the precondition. It must thus be satisfied before the loop has been executed.

The Loop

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.

Postcondition

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.

Loop Invariant Example

Let us use the above steps to construct a loop invariant for the example to the left. In the first step we observe that the loop termination condition is x < s.length() and we increase x every loop iteration with the statement x = x + 1. This means that the loop will terminate as at some point it will hold that x == s.length(). The adapted loop termination condition is thus x <= s.length() which we add to the loop invariant.

Loop Inv. 1: x <= s.length()

We then continue with step 2. We observe that the postcondition is count(s, c) == n and every time we find the char stored in c in the string s (s.charAt(x) == c) we increase n by one (n = n + 1). We can hence adapt the postcondition such that it holds for a substring of the string s. The substring is given the positional value x a s s.substring(0, x). We then, as is often done, introduce a descriptive function count to denote counting the occurences of the character in the variable c in the substring s.substring(0, x). This number should be equal to n after every iteration of the loop. This yields

Loop Inv. 2: x <= s.length() && count(s.substring(0, x), c) == n

In the next step we now add all the conditions imposed on the variable by usage of methods. Using length() requires s to be non-null, hence we add s != null. We must also add that x >= 0 as otherwise the s.charAt(x) method produces an error.

Loop Inv. 3: 0 <= x && s != null && x <= s.length() && count(s.substring(0, x), c) == n