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
>
|
