Lab 6

Consider the following app.

public class Main {
    public static void main(String[] args) {
        System.out.println(StrictMath.cbrt(4.4));
    }
}

If we run JPF with the following configuration file

target=Main
classpath=(directory that contains Main.class)

then we obtain output similar to the following.

JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Main.main()

====================================================== search started: 3/12/17 9:55 PM

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.cbrt
        at java.lang.StrictMath.cbrt(no peer)
        at Main.main(Main.java:6)
...

• Implement a native peer class. Add to the native peer a call to println with “native peer class” so that JPF produces the following output for the above app.

  JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
  
  
  ====================================================== system under test
  Main.main()
  
  ====================================================== search started: 3/12/17 9:59 PM
  native peer class
  1.6386425412012917
  
  ====================================================== results
  no errors detected
  ...

  Submit your native peer class and your configuration file (name it Main-native-peer.jpf).

• Implement a peer class. Add to the peer class a call to println with “peer class” so that JPF produces output for the above app similar to the following. Information about the cubic root can be found here. Ensure that the modelled cbrt method satisfies the specification given in the API of the StrictMath class. Some methods in the Double class might be useful.

  JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
  
  
  ====================================================== system under test
  Main.main()
  
  ====================================================== search started: 3/12/17 10:06 PM
  peer class
  1.6386425412012982
  
  ====================================================== results
  no errors detected
  ...

  Submit your peer class <b>and</b> your configuration file (name it Main-model-class.jpf).

To compile your classes, you may want to use

javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. (class name).java

or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.

To receive feedback, submit both classes and configuration files using

submit 4315 lab6 (name of file)

before Tuesday March 6.