Differences

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

--- lab8 [2018/02/25 14:53] – franck
+++ lab8 [2020/02/29 21:15] (current) – franck
@@ Line 1: / Line 1: @@
-====== Lab 6 ======
+~~NOTOC~~
+====== Lab 5 ======
 Consider the following app.
@@ Line 5: / Line 7: @@
 public class Main {
     public static void main(String[] args) {
-        System.out.println(StrictMath.cbrt(4.4));
+         System.out.println(StrictMath.exp(23.7));
     }
 }
@@ Line 13: / Line 15: @@
 <code>
 target=Main
-classpath=.
+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.
+JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.
@@ Line 23: / Line 25: @@
 Main.main()
-====================================================== search started: 3/12/17 9:55 PM
+====================================================== search started: 2/29/20 4:01 PM
 ====================================================== error 1
 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
-java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.cbrt
+java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.exp
-        at java.lang.StrictMath.cbrt(no peer)
+        at java.lang.StrictMath.exp(gov.nasa.jpf.vm.JPF_java_lang_StrictMath)
-        at Main.main(Main.java:6)
+        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>
-  * 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>
+===== Approach 1: native peer =====
-JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
+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.
@@ Line 40: / Line 68: @@
 Main.main()
-====================================================== search started: 3/12/17 9:59 PM
+====================================================== search started: 2/29/20 4:02 PM
 native peer
-.6386425412012917
+.9623624323651344E10
 ====================================================== results
 no errors detected
-...
-</code>Submit your native peer class <b>and</b> your configuration file (name it Main-native-peer.jpf).
+====================================================== statistics
-  * 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.<code>
+elapsed time:       00:00:00
-JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
+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.
@@ Line 55: / Line 107: @@
 Main.main()
-====================================================== search started: 3/12/17 10:06 PM
+====================================================== search started: 2/29/20 4:05 PM
-peer class
+[WARNING] orphan NativePeer method: java.lang.StrictMath.log(D)D
-.6386425412012982
+peer
+.9623624323651325E10
 ====================================================== 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
+====================================================== statistics
-<code>
+elapsed time:       00:00:00
-javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. (class name).java
+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>
-or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.
-, submit both classes and configuration files using
+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>
-submit 4315 lab6 (name of file)
+JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.
-</code>
+====================================================== 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
-Consider the following app.
+====================================================== statistics
-<html>
+elapsed time:       00:00:00
-<pre>
+states:             new=1,visited=0,backtracked=1,end=1
-public class ComputeSquareRoot {
+search:             maxDepth=1,constraints=0
-    public static void main(String[] args) {
+choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
-          double data = 3.1415926;
+heap:               new=555,released=13,maxLive=0,gcCycles=1
-          System.out.println("The square root of " + data + " is " + StrictMath.sqrt(data));
+instructions:       9955
-    }
+max memory:         240MB
-}
+loaded code:        classes=62,methods=1399
-</pre>
-</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.
+====================================================== search finished: 2/29/20 4:10 PM
-  - Develop a native peer so that the above app can be verified with JPF.
+</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