Consider the following app.

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

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 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.


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

====================================================== search started: 2/29/20 4:01 PM

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.exp
        at java.lang.StrictMath.exp(gov.nasa.jpf.vm.JPF_java_lang_StrictMath)
        at Main.main(Main.java:3)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
        at java.lang.StrictMath.exp(StrictMath.java)
        at Main.main(Main.java:3)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=0,end=0
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=369,released=0,maxLive=0,gcCycles=0
instructions:       3182
max memory:         240MB
loaded code:        classes=66,methods=1427

====================================================== search finished: 2/29/20 4:01 PM

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

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


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

====================================================== search started: 2/29/20 4:02 PM
native peer
1.9623624323651344E10

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=353,released=11,maxLive=0,gcCycles=1
instructions:       3189
max memory:         240MB
loaded code:        classes=62,methods=1399

====================================================== search finished: 2/29/20 4:02 PM

To compile your class, 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.

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” so that JPF produces output for the above app similar to the following. To model exp, you may want to use a Taylor series. Ensure that the modelled exp 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 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.


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

====================================================== search started: 2/29/20 4:05 PM
[WARNING] orphan NativePeer method: java.lang.StrictMath.log(D)D
peer
1.9623624323651325E10

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=355,released=11,maxLive=0,gcCycles=1
instructions:       5184
max memory:         240MB
loaded code:        classes=62,methods=1331

====================================================== search finished: 2/29/20 4:05 PM

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

Use jpf-nhandler so that JPF produces the following output.

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


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

====================================================== search started: 2/29/20 4:10 PM
* DELEGATING Unhandled Native -> java.lang.StrictMath.exp
1.9623624323651344E10

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=555,released=13,maxLive=0,gcCycles=1
instructions:       9955
max memory:         240MB
loaded code:        classes=62,methods=1399

====================================================== search finished: 2/29/20 4:10 PM

Submit your configuration file (name it Main-nhandler.jpf).

To receive feedback, submit your classes and configuration files using

submit 4315 lab5 (name of file)

before Thursday March 12.