doc/intro/random_example.md

   1 # Example: `java.util.Random` #
   2
   3 We start with a simple example that uses java.util.Random. Consider the following program that obtains two random values in (2) and (3), and then performs some computation (4) with them.
   4
   5 ~~~~~~~~ {.java}
   6 import java.util.Random;
   7
   8 public class Rand {
   9      public static void main (String[] args) {
  10           Random random = new Random(42);      // (1)
  11
  12           int a = random.nextInt(2);           // (2)
  13           System.out.println("a=" + a);
  14
  15           //... lots of code here
  16
  17           int b = random.nextInt(3);           // (3)
  18           System.out.println("  b=" + b);
  19
  20           int c = a/(b+a -2);                  // (4)
  21           System.out.println("    c=" + c);
  22      }
  23 }
  24 ~~~~~~~~
  25
  26
  27 ## Testing ##
  28
  29 Executing this program with a normal Java VM yields something like the following output. If we don't provide an explicit seed when creating the Random object in (1), the result is going to differ between runs, but every run will choose just a single `a` and `b` value (i.e. print just a single `"a=.."` and `"b=.."` line.
  30
  31 ~~~~~~~~ {.java}
  32 > java Rand
  33 a=1
  34   b=0
  35     c=-1
  36 >
  37 ~~~~~~~~
  38
  39 Let's look at a graphical representation of all the ways our program could be executed, and how it actually was executed in our test run. The nodes of the graph represent *program states*, and the edges *transitions* the execution could take from a certain state.
  40
  41 ![Figure 1: Random example](../graphics/sw-model-checking.svg){align=center width=700}
  42
  43 ## Model Checking ##
  44
  45 Enter JPF - not much different results if we start JPF as a plain 'java' replacement. The only difference is that it (a) takes longer to complete, and (b) tells us something about a "search", which hints on that something more than in our test run is going on
  46
  47 ~~~~~~~~ {.bash}
  48 > bin/jpf Rand
  49 JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
  50 ====================================================== system under test
  51 application: /Users/pcmehlitz/tmp/Rand.java
  52
  53 ====================================================== search started: 5/23/07 11:48 PM
  54 a=1
  55   b=0
  56     c=-1
  57
  58 ====================================================== results
  59 no errors detected
  60
  61 ====================================================== search finished: 5/23/07 11:48 PM
  62 >
  63 ~~~~~~~~
  64
  65 What is this "search" supposed to mean? Looking at source line (4) we realize that there is a potential problem: for certain `a` and `b` values, this expression can cause a division by zero `ArithmeticException`. Depending on the random seed used in (1), it's quite possible we would never encounter this case if we run (i.e. test) the program with a normal JVM.
  66
  67 Re-enter JPF - but this time we tell it to not only consider single values for `a` and `b`, but look at all possible choices:
  68
  69 ~~~~~~~~ {.bash}
  70 > bin/jpf +cg.enumerate_random=true Rand
  71 JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
  72 ====================================================== system under test
  73 application: /Users/pcmehlitz/tmp/Rand.java
  74
  75 ====================================================== search started: 5/23/07 11:49 PM
  76 a=0
  77   b=0
  78     c=0
  79   b=1
  80     c=0
  81   b=2
  82
  83 ====================================================== error #1
  84 gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
  85 java.lang.ArithmeticException: division by zero
  86         at Rand.main(Rand.java:15)
  87 ....
  88 >
  89 ~~~~~~~~
  90
  91 What has happened? By specifying "+vm.enumerate_random=true" we told JPF to consider all possible values for expressions (2) and (3). JPF starts with `"a=0"`, then picks `"b=0"`, which yields a valid `"c=0"` value. But instead of terminating like a normal VM, JPF recognized that there are more choices left, so it backtracks to (3) and picks `"b=1"`. Again, no problem here with computing `"c=0"`. Back to (3), JPF now tries `"b=2"`, which of course spells disaster for our little program when executing (4), as can be seen by the following error report.
  92
  93 Here is a graphical representation of this search process. It should be noted that JPF per default only runs up to the point where it finds an error or there are no more choices left to explore. But if we would somehow fix the `"a=0,b=2"` case, JPF would still find the `"a=1,b=1"` case in the next run, since it systematically tries all choices. No matter what error it finds, JPF also keeps the complete trace (execution path) how it got to this error (denoted by the red arrows), which means we don't have to debug the program to find out.
  94
  95 ![Figure 2: Random example](../graphics/sw-model-checking-2.svg){align=center width=450}