[Javapathfinder-user] Generating counter examples

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

Hi!

I'm interested in usping JPF for generating counter examples. I've
read a paper titled "Test Input Generation with Java Pathfinder" but
my limited knowledge of JPF itself is a hinderance towards using it
for my purpose.

Can somebody guide me what I should be reading for generating
counterexamples? An interesting example of what I want to do can be:

The following code swaps two positions in an integer array.

a[i] +=3D a[j];
a[j] =3D a[i] - a[j];
a[i] -=3D a[j];

However, it fails to swap the positions when i and j both point to the
same element, i.e., i =3D j (of course there are other problems like
array index out of bound, etc. but that can be handled by pre
conditions).

Any help will be highly appreciated.

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