Differences

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

--- lab8 [2016/03/03 13:46] – franck
+++ lab8 [2017/03/02 15:00] – franck
@@ Line 1: / Line 1: @@
-Implement a listener and publisher that, given the following app,
+====== Lab 8 ======
+Consider the following app.
 <html>
 <pre>
-import java.util.Random;
+public class ComputeSquareRoot {
-public class Example {
     public static void main(String[] args) {
-	Random random = new Random();
+          double data = 3.1415926;
-	if (random.nextBoolean()) {
+          System.out.println("The square root of " + data + " is " + StrictMath.sqrt(data));
-	    System.out.println("true");
-	} else {
-	    System.out.println("false");
-	}
     }
 }
 </pre>
 </html>
-and the application configuration file
-<html>
-<pre>
-target=Example
-classpath=.
-native_classpath=.
-listener=AmountOfNonDeterminism
-cg.enumerate_random=true
-</pre>
-</html>
-produces output similar to
-<html>
-<pre>
-JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
+  - 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.
-====================================================== system under test
+  - Develop a native peer so that the above app can be verified with JPF.
-Example.main()
-====================================================== search started: 3/2/16 2:27 PM
-false
-true
-======================================================
-maximum amount of nondeterminism: 2 choice(s)
-====================================================== 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=352,released=12,maxLive=0,gcCycles=1
-instructions:       3176
-max memory:         56MB
-loaded code:        classes=61,methods=1332
-====================================================== search finished: 3/2/16 2:27 PM
-</pre>
-</html>
-That is, JPF reports the maximum amount of nondeterminism (maximum number of outgoing transitions from any state of the system under test).
-Apart from the classes that have been discussed in the lectures, also the class ChoiceGenerator, which is part of the package gov.nasa.jpf.vm, may be useful.