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
|
