[Javapathfinder-user] Re: JPF for Methods?

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

Ok, here is my reply. Please correct me if I am wrong.

Currently you have to write instrumentation code; to exhaustively test
everything, use Verify.random() for generating integers and booleans.
The same code can be rewritten as follows:

import gov.nasa.jpf.jvm.Verify;

public class MaxWhile {
    public static 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[]) {
=09int [] myArray =3D new int [Verify.random(10)];
=09if (myArray.length <=3D 1) return;

=09for (int i=3D0; i<myArray.length; i++)=20
=09    myArray [i] =3D Verify.random(10);

=09int max =3D findMax (myArray);
=09for (int i=3D0; i<myArray.length; i++)=20
=09    assert (max >=3D myArray[i]);
    }
}

This can be compiled with javac by having gov.nasa.jpf.jvm.Verify in
classpath. Run jpf on the class file. The error trace has Random#i at
different points which collectively comprise the counterexample.
Perhaps, at present there is no easier way of looking at the
assignment of the variables in the form of a "watch window" of a
standard debugger.

/Ali
--=20
IMP Student
Dependable Computer Systems
Chalmers University of Technology, Sweden


On 7/19/05, Muhammad Ali Shah <muh...@gm...> wrote:
> Hi,
>=20
> Is it possible to verify methods without any invokation code? For
> example, consider the following class:
>=20
> public class Main {
>     public int findMax (int []a) {
>         int k =3D 1;
>         int max =3D a[1];
>=20
>         while (k < a.length) {
>             if (a[k] > max) max =3D a[k];
>             k++;
>         }
>=20
>         return max;
>     }
>=20
>     public static void main (String args[]) {
>     }
> }
>=20
>=20
> 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).
>=20
> Is it possible to check the index out of bound issue with JPF? Any
> hints will be highly appreciated.
>=20
> /Ali
>