[Javapathfinder-user] JPF for Methods?

[Muhammad A. S. <muh...@gm...>]

Hi,

Is it possible to verify methods without any invokation code? For
example, consider the following class:

public class Main {
    public int findMax (int []a) {
=09int k =3D 1;
=09int max =3D a[1];

=09while (k < a.length) {
=09    if (a[k] > max) max =3D a[k];
=09    k++;
=09}

=09return max;
    }

    public static void main (String args[]) {
    }
}


The method findMax will throw exception if invoked with an array of
size 1. Also, it fails to find the maximum element when the max
element is at index 0 (but for that we would be required to specify
the property in some way).

Is it possible to check the index out of bound issue with JPF? Any
hints will be highly appreciated.

/Ali