lab8
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
lab8 [2016/03/02 21:09] – 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 | ||
< | < | ||
<pre> | <pre> | ||
- | import java.util.Random; | + | public class ComputeSquareRoot |
- | + | ||
- | public class Example | + | |
public static void main(String[] args) { | public static void main(String[] args) { | ||
- | Random random | + | double data = 3.1415926; |
- | if (random.nextBoolean()) { | + | System.out.println(" |
- | | + | |
- | } else { | + | |
- | System.out.println(" | + | |
- | } | + | |
} | } | ||
} | } | ||
</ | </ | ||
</ | </ | ||
- | and the application configuration file | ||
- | < | ||
- | <pre> | ||
- | target=Example | ||
- | classpath=. | ||
- | native_classpath=. | ||
- | listener=AmountOfNonDeterminism | ||
- | cg.enumerate_random=true | ||
- | </ | ||
- | </ | ||
- | produces output similar to | ||
- | < | ||
- | <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. | |
- | ====================================================== 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: | + | |
- | + | ||
- | ====================================================== results | + | |
- | no errors detected | + | |
- | + | ||
- | ====================================================== statistics | + | |
- | elapsed time: | + | |
- | states: | + | |
- | search: | + | |
- | choice generators: | + | |
- | heap: new=352, | + | |
- | instructions: | + | |
- | max memory: | + | |
- | loaded code: classes=61, | + | |
- | + | ||
- | ====================================================== 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 | + | |
- | Try not to hard-code ====================================================== but | + | |
- | use an appropriate methods provided by JPF. | + | |
lab8.txt · Last modified: 2017/03/03 15:55 by franck