EECS4315

User Tools

Site Tools

You are here: Mission Critical Systems » Lab 5
Trace:
lab8

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
lab8 [2017/03/02 15:00] – francklab8 [2020/02/29 21:15] (current) – franck
Line 1: Line 1:
-====== Lab 8 ======+~~NOTOC~~
  
 +====== Lab 5 ======
  
 Consider the following app. Consider the following app.
-<html> +<code java> 
-<pre> +public class Main {
-public class ComputeSquareRoot {+
     public static void main(String[] args) {     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>+ 
 +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 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 
 +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 
 +</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 
 +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 
 +</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 
 +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 
 +</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.
  
-  - 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. 
-  - Develop a native peer so that the above app can be verified with JPF. 
  
lab8.1488466854.txt.gz · Last modified: by franck