[Javapathfinder-user] Array of Double Question

[Chiu C. T. <cc...@cs...>]

Hi

I experimenting with Java Pathfinder for a class and came across a
strange behaviour.
In a nutshell, I have an array of 4 doubles, [0.0, 1.0, 2.0, 3.0] and I
want to swap the first element with the
third element. So the final result should be [0.0, 3.0, 2.0, 1.0].

However, running this simple code through jpf shows that after the swap,
the array becomes
[0.0, 3.0, 0.0, 1.0]

(The actual values are a little different, I just rounded them up for
clarity.)
Does anyone have an explanation for this?

Thanks
Chiu



I have attached a copy of the code and the output below.

--------------------------------------------------------------------------
Code:
import gov.nasa.jpf.jvm.Verify;
import java.util.Random;

public class Swap {

    public static void main (String[] args) {
        double[] numbers;
        numbers = new double[4];

        numbers[0] = 0.0;
        numbers[1] = 1.0;
        numbers[2] = 2.0;
        numbers[3] = 3.0;

        Verify.instrumentPoint("pre-sort");

System.out.print("1) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        double t = numbers[1];

System.out.print("t is "+t+"\n");
System.out.print("2) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        numbers[1] = numbers[3];

System.out.print("3) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        numbers[3] = t;

System.out.print("numbers[1] is "+numbers[1]+" and numbers[3] is
"+numbers[3]+"\n");
System.out.print("4) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        Verify.instrumentPoint("post-sort");

System.out.print("After\n");
System.out.print(numbers[0] + ", " + numbers[1] + ", " + numbers[2] + ",
" + numbers[3] +"\n\n");
    }
}
-------------------------------------------------------------------------------------------------------------

Output:

Java Pathfinder Model Checker v3.1.2 - (C) 1999-2005 RIACS/NASA Ames
Research Center
1) 5.299808824E-315, 1.000000238418579, 2.000000477069989, 3.0

t is 1.000000238418579
2) 5.299808824E-315, 1.000000238418579, 2.000000477069989, 3.0

3) 5.307579804E-315, 3.0, 5.307579804E-315, 3.0

numbers[1] is 3.0 and numbers[3] is 1.000000238418579
4) 5.307579804E-315, 3.0, 5.299808824E-315, 1.000000238418579

After
5.307579804E-315, 3.0, 5.299808824E-315, 1.000000238418579

------------------------------------ thread stacks
Thread: main
        at Swap.main(Swap.java:8)

------------------------------------ end thread stacks


===================================
  No Errors Found
===================================