Differences

This shows you the differences between two versions of the page.

--- lab8 [2017/03/03 15:55] – franck
+++ lab8 [2020/02/29 21:15] (current) – franck
@@ Line 1: / Line 1: @@
-====== Lab 8 ======
+~~NOTOC~~
+====== Lab 5 ======
 Consider the following app.
-<html>
+<code java>
-<pre>
+public class Main {
-public class ComputeSquareRoot {
     public static void main(String[] args) {
-          double data = 3.1415926;
+         System.out.println(StrictMath.exp(23.7));
-          System.out.println("The square root of " + data + " is " + StrictMath.sqrt(data));
     }
 }
-</pre>
+</code>
-</html>
-  - Develop a model class so that the above app can be verified with JPF.  [[https://en.wikipedia.org/wiki/Methods_of_computing_square_roots|This]] Wikipedia page might be helpful.
+If we run JPF with the following configuration file
-  - Develop a native peer so that the above app can be verified with JPF.
+<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 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
+</code>
+===== Approach 1: native peer =====
+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.
+<code>
+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
+.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
+</code>
+To compile your class, 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.
+Submit your native peer class **and** your configuration file (name it Main-native-peer.jpf).
+===== Approach 2: peer =====
+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 [[https://en.wikipedia.org/wiki/Taylor_series|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.
+<code>
+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
+.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
+</code>
+Submit your peer class **and** your configuration file (name it Main-peer.jpf).
+===== Approach 3: jpf-nhandler =====
+Use jpf-nhandler so that JPF produces the following output.
+<code>
+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
+.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
+</code>
+Submit your configuration file (name it Main-nhandler.jpf).
+To receive feedback, submit your classes and configuration files using
+<code>
+submit 4315 lab5 (name of file)
+</code>
+before Thursday March 12.
-To receive feedback, submit your code using the submit command before Tuesday March 7:
-submit 4315 lab8 <name of class>.java