Common Example‎ > ‎

ArrayMax in KIV

The project files are located under projects/Exercise8/specs/ArrayMax/

The implementation is:

public class ArrayMax {

    public static int maxWhile(int[] a) {
        if ( a.length == 0 ) return 0;
        int max = a[0], i = 1;
        while ( i < a.length ) {
           if ( a[i] > max ) max = a[i];
           ++i;
        }
        return max;
    }

}


The proof obligation (Gentzen-style sequent) is:
st[_mode] = noval, okarray(a, int_type, st), init(st) ⊢ <st; private (int i, int[] a) i = swt.ArrayMax.maxWhile(a);> i = max(getintarray(a, st)) ;

The used loop invariant is:
                              (  0 < i1
                               ∧ i1 ≤ st[a0 -- _length] .intval
                               ∧ st[_mode] = noval ∧ a0 ≠ jvmref
                               ∧ okarray(a0, int_type, st) ∧ init(st)
                               ∧ a = a0
                               ∧ int_max0  = max(getintarray(a0, 0, i1, st)))
Comments