====== Lab 6 ======

Consider the following app.
<code java>
public class Main {
    public static void main(String[] args) {
        System.out.println(StrictMath.cbrt(4.4));
    }
}
</code>

If we run JPF with the following configuration file
<code>
target=Main
classpath=(directory that contains Main.class)
</code>
then we obtain output similar to the following.
<code>
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)
...
</code>

  * 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.<code>
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
...
</code>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 {{https://en.wikipedia.org/wiki/Cube_root|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.<code>
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
...
</code>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
<code>
javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. (class name).java
</code>
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
<code>
submit 4315 lab6 (name of file)
</code>
before Tuesday March 6.