In continuation to the proof obligation posted last week, I decided to explore loop invariants. This means converting the

Now, this is much easier to prove if we can select a proper loop invariant.

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

There are two subcases (amongst others) generated by KeY when a loop invariant is used:

But termination is not easy to show unless we can somehow tell that

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:

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

Once we have proved everything regarding the invariant, we can

Thus, the fourth case, called

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

*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

**the invariant to prove the real thing, which was the following first order logical formula:***use*\forall int i; (i < a.length & i >= 0 -> max >= a[i] )

Thus, the fourth case, called

**Use Case**is something of the formk > 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.
## No comments:

## Post a Comment