Proving Loops with Loop Invariants

In continuation to the proof obligation posted last week, I decided to explore loop invariants. This means converting the for loop in the code to a while one. The new proof obligation is as follows:

\problem {
\<{ int[] a; int max; }\>
(
 (!a = null & a.length > 0) ->
 (
  \<{ 
   max = a[0];
   int k = 1;
   while (k < a.length) {
    if (a[k] > max) max = a[k];
    k++;
   }
  }\>
  \forall int i; (i < a.length & i >= 0 -> max >= a[i] )
 )
)
}

Now, this is much easier to prove if we can select a proper loop invariant. What is it that holds before the loop starts execution, remains true after each iteration and holds even after the loop termination? A good first attempt can be

\forall int i; (i >= 0 & i < k -> max >= a[i])

Again, the syntax is specific to KeY but the semantics are valid for any theorem prover for imperative languages. A stronger invariant can be more useful and in fact, in this particular example, the loop invariant can be strengthened to

k > 0 & k <= a.length & 
\forall int i; (i >= 0 & i < k -> max >= a[i])

There are two subcases (amongst others) generated by KeY when a loop invariant is used: Invariant Initially Valid and Body Preserves Invariant. Since we are dealing with necessity (signified by <code in angle brackets>), and not with just a possibility, we have to show termination of the loop as well. In other words, we have to show that the loop terminates and, after termination, the formula holds. Thus, the third case to prove is Termination.

Invariant Initially Valid:
 a.length >  0
==>
 \forall int i;  (i >= 0 & i <  1 -> a[0] >= a[i])


Body Preserves Invariant:
   _k >  0
 & _k <= a.length
 & \forall int i; 
     (i >= 0 & i <  _k -> _max >= a[i]),
 a.length >  0
==>
 {
   k:=_k,
   max:=_max}
   \[{method-frame(()): {
             if (k < a.length) {
                if (a[k] > max)
                   max=a[k];
                k++;
             }
       }
     }\] (\forall int i; (i >= 0 & i <  a.length -> max >= a[i])
  }

But termination is not easy to show unless we can somehow tell that something is gradually approaching towards a limit which will make the while statement false. This is where the concept of Variant is Decreasing comes in. In KeY, we can define that a.length - k is decreasing with each iteration of the loop. With the help of this statement (which of course, we have to prove separately), Termination subgoal takes the following form:

(a.length - _k) <= 0
==>
 {k:=_k,
  max:=_max}
  \<{
      while ( k < a.length ) {
         if (a[k]>max)
           max=a[k];
         k++;
      }
  }\> true

This is, of course, very easy to prove because of the premises of the implication; the loop will not execute at all and there is no statement after the loop, Hence, the termination. But while doing this, we have introduced a new sub goal: Variant is Decreasing. We have to prove that with each iteration of the loop a.length - k is actually decreasing. This subgoal has the following form:

 _k_1 >  0,
 _k_1 <= a.length,
 \forall int i;  (i >= 0 & i <  _k_1 -> _max_1 >= a[i]),
 {k:=_k_1}
   \<{method-frame(()): {
         var=k       }
     }\> var = TRUE,
 a.length >  0
==>
 {k:=_k_1,
   max:=_max_1,
   var_1:=a.length - _k_1}
   \<{
        if (a[k]>max)
          max=a[k];
        k++;
     }\> (a.length - k) <  var_1

It looks daunting but after symbolic execution of the code, it's pretty simple.

Once we have proved everything regarding the invariant, we can use the invariant to prove the real thing, which was the following first order logical formula:

\forall int i; (i < a.length & i >= 0 -> max >= a[i] )

Thus, the fourth case, called Use Case is something of the form

k > 0 & k <= a.length & 
\forall int i; (i >= 0 & i < k -> max >= a[i]) ==>
\forall int i; (i < a.length & i >= 0 -> max >= a[i] )

which is much easier to prove than the standalone formula that we initially had.

---

My affair with loop invariants was a very short one. Perhaps, I'll come back to these in future. At present, I'm moving on to manually injecting bugs in this code and trying to find them using KeY.