EECS4315

User Tools

Site Tools

You are here: Mission Critical Systems » Lab 6
Trace: • Quiz 5 • Forums • Quiz 1 • Quiz 2 • Resources • final • Quiz 6 • Quiz 4 • Lab 10 • Lab 6
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 [2018/02/25 14:53] – francklab8 [2018/02/25 15:00] (current) – franck
Line 13: Line 13:
 <code> <code>
 target=Main target=Main
-classpath=.+classpath=(directory that contains Main.class)
 </code> </code>
 then we obtain output similar to the following. then we obtain output similar to the following.
Line 33: Line 33:
 </code> </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>+  * Implement a native peer class.  Add to the native peer a call to println with "native peer class" so that JPF produces the following output for the above app.<code>
 JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 41: Line 41:
  
 ====================================================== search started: 3/12/17 9:59 PM ====================================================== search started: 3/12/17 9:59 PM
-native peer+native peer class
 1.6386425412012917 1.6386425412012917
  
Line 47: Line 47:
 no errors detected no errors detected
 ... ...
-</code>Submit your native peer class <b>and</b> your configuration file (name it Main-native-peer.jpf). +</code>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 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>+  * 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 {{https://en.wikipedia.org/wiki/Cube_root|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>
 JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 70: Line 70:
 or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse. or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.
  
-, submit both classes and configuration files using+To receive feedback, submit both classes and configuration files using
 <code> <code>
 submit 4315 lab6 (name of file) submit 4315 lab6 (name of file)
 </code> </code>
 +before Tuesday March 6.
  
- 
- 
- 
- 
-Consider the following app. 
-<html> 
-<pre> 
-public class ComputeSquareRoot { 
-    public static void main(String[] args) { 
-          double data = 3.1415926; 
-          System.out.println("The square root of " + data + " is " + StrictMath.sqrt(data)); 
-    } 
-} 
-</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. 
-  - Develop a native peer so that the above app can be verified with JPF. 
- 
-To receive feedback, submit your code using the submit command before Tuesday March 7:\\ 
-submit 4315 lab8 <name of class>.java  
  
lab8.1519570434.txt.gz · Last modified: by franck