Corrected some show examples

Author: davidcok

tutorial/Debugging.md

@@ -15,7 +15,7 @@ First note that there are different kinds of problems that can lead to a failed
 * The prover is missing some vital information that prevents it from making the necessary proof steps. For this situation you can add lemmas or other assumptions [here](Lemmas).
 
 It is worth restating a few points:
-* Just because a specification and implementation agree (`openjml` verifies) does not mean that they are correct. They could still be both wrong in the same way compared to what is really desired of the program. Careful human review and understanding of requirements cannot replace either traditional testing or verification, though both of those are necessary in giving confidence in a program's correctness.
+* Just because a specification and implementation agree (`openjml` verifies) does not mean that they are correct. They could still be both wrong in the same way compared to what is really desired of the program. Careful human review and understanding of requirements cannot be replaced by either traditional testing or verification, though both of those are necessary in giving confidence in a program's correctness.
 * The techniques presented here are largely specific to `openjml`, at least in the details. Each tool and prover has different ways in which it has difficulties, though some general ideas and techniques may translate from one situation to another.
 * Start with simple problems, understand them well, and then move on to complex situations.
 

tutorial/InspectingCounterexamples.md

@@ -25,7 +25,7 @@ which produces
 {% include_relative T_show2.out %}
 ```
 The values shown are the result of a non-deterministic search; they might very well be different values on subsequent runs.
-Nevertheless, for the values of `a`, `b`, `c`, and `d` shown here, the result is equal to `b` or `d`, instead of, for these values, the value of `a`.
+Nevertheless, for the values of `a`, `b`, `c`, and `d` shown here, the result is equal to `b`, instead of, for these values, the value of `d`.
 Some code inspection shows that there is a cut&paste error on line 9.
 
 The counterexample is always in terms of concrete values --- that is how the underlying solvers work. One would much rather have a symbolic condition that represents the cases that fail, but that is beyond the current state of the art. At present, the best one can do is do some human induction based on a few examples to understand when a program or its specification fails.

tutorial/MethodSelection.md

@@ -11,11 +11,16 @@ First, remember that the `OpenJML` command-line lists options (and their values)
 just like the Java compiler (`javac`) does. Usually though you have a set of interdependent files
 together in one folder. So `OpenJML` allows you to put a folder path on the command-line,
 after the `--dir` option, as in `openjml --esc --dir ~/myfiles`. You can use the `--dirs` option
-to list several files: `openjml --esc --dirs ~/myfiles1 ~/myfiles2 ~/myfiles3`. Listing a 
+to list several folders: `openjml --esc --dirs ~/myfiles1 ~/myfiles2 ~/myfiles3`. Listing a 
 folder name includes subfolders recursively by default. If you don't want recursion, then list
 the files using a wildcard as in `~/myfiles/*.java`. The `--dirs` option interprets all
 successive command-line arguments as folder paths, up to an argument that begins with a hyphen (`-`).
 
+## Specific files
+
+If you are only interested in proofs of methods within a given file, then list just that file on
+the command-line and make sure that any other needed file is present on the sourcepath or the classpath.
+
 ## Specific methods
 
 To limit proof attempts to specific methods, use the `--method` and `--exclude` options.
@@ -30,4 +35,4 @@ a prepended fully-qualified class name or an appended argument signature, as in
 `--method="mypackage.MyClass.myMethod"` or `--method="myMethod(int,java.lang.String)"`. Note that
 when the expanded name includes characters interpreted by the shell, such as periods and
 parentheses, quotes around the method name are needed.
-* More complicated strings that include wildcards for matching are described in the Ope JML Users' Guide.
+* More complicated strings that include wildcards for matching are described in the OpenJML Users' Guide.

tutorial/T_show2.java

@@ -6,7 +6,7 @@ int max(int a, int b, int c, int d) {
     int maxSoFar = a;
     if (b > maxSoFar) maxSoFar = b;
     if (c > maxSoFar) maxSoFar = c;
-    if (d > maxSoFar) maxSoFar = b;
+    if (d > maxSoFar) maxSoFar = c;
     //@ show a, b, c, d, maxSoFar;
     return maxSoFar;
   }

tutorial/T_show2.out

@@ -1,16 +1,16 @@
-T_show2.java:10: verify: Show statement expression a has value ( - 2147480361 )
+T_show2.java:10: verify: Show statement expression a has value ( - 282 )
     //@ show a, b, c, d, maxSoFar;
              ^
-T_show2.java:10: verify: Show statement expression b has value ( - 2147480362 )
+T_show2.java:10: verify: Show statement expression b has value ( - 281 )
     //@ show a, b, c, d, maxSoFar;
                 ^
-T_show2.java:10: verify: Show statement expression c has value ( - 2147477363 )
+T_show2.java:10: verify: Show statement expression c has value 1
     //@ show a, b, c, d, maxSoFar;
                    ^
-T_show2.java:10: verify: Show statement expression d has value ( - 2147477362 )
+T_show2.java:10: verify: Show statement expression d has value 2
     //@ show a, b, c, d, maxSoFar;
                       ^
-T_show2.java:10: verify: Show statement expression maxSoFar has value ( - 2147480362 )
+T_show2.java:10: verify: Show statement expression maxSoFar has value 1
     //@ show a, b, c, d, maxSoFar;
                          ^
 T_show2.java:11: verify: The prover cannot establish an assertion (Postcondition: T_show2.java:3:) in method max

tutorial/T_show4.java

@@ -1,4 +1,4 @@
-// openjml --esc T_show4.java
+// ## openjml --esc T_show4.java
 public class T_show4 {
   //@ public invariant data.length >= 10;
   //@ spec_public

tutorial/T_show6.out

@@ -9,52 +9,27 @@ TRACE of T_show1.max(int,int,int,int)
 T_show1.java:1: 	requires true; 
 			VALUE: true	 === true
 T_show1.java:6: 	int maxSoFar = a
-			VALUE: a	 === ( - 8946 )
-			VALUE: maxSoFar	 === ( - 8946 )
+			VALUE: maxSoFar	 === ( - 536 )
 T_show1.java:7: 	if (b > maxSoFar) ...
-			VALUE: b	 === ( - 8945 )
-			VALUE: maxSoFar	 === ( - 8946 )
 			VALUE: b > maxSoFar	 === true
 			VALUE: (b > maxSoFar)	 === true
 				Condition = true
 T_show1.java:7: 	maxSoFar = b
-			VALUE: b	 === ( - 8945 )
-			VALUE: maxSoFar = b	 === ( - 8945 )
+			VALUE: maxSoFar = b	 === ( - 535 )
 T_show1.java:8: 	if (c > maxSoFar) ...
-			VALUE: c	 === 1
-			VALUE: maxSoFar	 === ( - 8945 )
 			VALUE: c > maxSoFar	 === true
 			VALUE: (c > maxSoFar)	 === true
 				Condition = true
 T_show1.java:8: 	maxSoFar = c
-			VALUE: c	 === 1
 			VALUE: maxSoFar = c	 === 1
 T_show1.java:9: 	if (d > maxSoFar) ...
-			VALUE: d	 === 2
-			VALUE: maxSoFar	 === 1
 			VALUE: d > maxSoFar	 === true
 			VALUE: (d > maxSoFar)	 === true
 				Condition = true
 T_show1.java:9: 	maxSoFar = c
-			VALUE: c	 === 1
 			VALUE: maxSoFar = c	 === 1
 T_show1.java:10: 	return maxSoFar;
-			VALUE: maxSoFar	 === 1
 T_show1.java:3: 	ensures \result >= a && \result >= b && \result >= c && \result >= d; 
-			VALUE: \result	 === 1
-			VALUE: a	 === ( - 8946 )
-			VALUE: \result >= a	 === true
-			VALUE: \result	 === 1
-			VALUE: b	 === ( - 8945 )
-			VALUE: \result >= b	 === true
-			VALUE: \result >= a && \result >= b	 === true
-			VALUE: \result	 === 1
-			VALUE: c	 === 1
-			VALUE: \result >= c	 === true
-			VALUE: \result >= a && \result >= b && \result >= c	 === true
-			VALUE: \result	 === 1
-			VALUE: d	 === 2
-			VALUE: \result >= d	 === false
 T_show1.java:10: Invalid assertion (Postcondition)
 : T_show1.java:3: Associated location
 

tutorial/TimeAndErrorLimits.md

@@ -22,7 +22,7 @@ find any more failures.
 However, the last step -- where no more assertion violations are found --
 can be time-consuming. So sometimes it is useful to stop after just one verification failure  (or a small fixed number) is reported.
 The number of errors reported for each method can be limited using the 
-`--escMaxWarnings` option. By default it is set to a very large number,
+`--esc-max-warnings` option. By default it is set to a very large number,
 but it is a reasonable working style to set it to 1.
 
 Note that there will be no proof attempts for any methods in a file if there

tutorial/type-bigint.md

@@ -20,7 +20,9 @@ type `\bigint` and `i` a value of a Java numeric type.
 * `j / k` is mathematical integer division (truncation toward zero); `k` must not be 0; `j/k` is negative or zero if `j` and `k` have different signs and is positive or zero if `j` and `k` have the same sign
 * `j % k` is mathematical integer modulo, but is similar to Java's `%` operation: `k` may not be zero, `j%k` has the same sign as `j` and is independent of the sign of `k`, and for `k != 0`, `(j/k)*k + (j%k) == j`
 * `<` and `<=` and `>` and `>=` have their expected meanings with the result type being boolean
-* casts are allowed to and from other numeric types, such as `(\bigint)i` or `(int)j`. When casting from `\bigint` to a bounded type, a range check is performed, depending on the [arithmetic mode](ArithmeticModes).
+* implicit conversions are allowed from Java integral types to `\bigint`
+* casts are allowed to and from other numeric types, such as `(\bigint)i` or `(int)j`. When casting from `\bigint` to a bounded type, a range check is performed, depending on the [arithmetic mode](ArithmeticModes); when casting from `\real`, `double`, or `float`, the value is truncated toward zero.
+* implicit conversion of `java.math.BigInteger` to `\bigint` is permitted; use `i.bigValue()` to convert a `\bigint` value `i` to `java.math.BigInteger`
 
 For example, one can write the following:
 ```

tutorial/type-real.md

@@ -17,9 +17,10 @@ type `\real`.
 * `j - k` is mathematical real subtraction
 * `j * k` is mathematical real multiplication
 * `j / k` is mathematical real division (not rounded to an integer); `k` must not be 0
-* `j % k` is mathematical real modulo, but is similar to Java's `%` operation: `k` may not be zero, `j%k` has the same sign as `j` and is independent of the sign of `k`, and for `k != 0`, `(j/k)*k + (j%k) == j`.
+* `j % k` is mathematical real modulo, but is similar to Java's `%` operation: `k` may not be zero, `j%k` has the same sign as `j` and is independent of the sign of `k`, and for `k != 0`, `((\bigint)(j/k))*k + (j%k) == j`.
 * `<` and `<=` and `>` and `>=` have their expected meanings with the result type being boolean
-* casts are allowed to and from other numeric types, such as `(\bigint)j`, which truncates towards zero.
+* implicit conversions are allowed from `double`, `real`, `\bigint` and Java integral types
+* explicit casts are allowed to and from other numeric types, such as `(\bigint)j`, which truncates towards zero.
 
 ```diff
 ! Caveat: Though real numbers are supported in OpenJML, the connection between real numbers and floating point numbers is incomplete and in some cases (such as handling NaN and infinite fp numbers) wrong
@@ -32,7 +33,7 @@ type `\real`.
 //@ set rr = r * 2;
 ```
 
-As for `\bigint`, many of the methods in `java.lang.Math` have been specified for `real` values:
+Just like for `\bigint`, many of the methods in `java.lang.Math` have been specified for `real` values:
 ```
 {% include_relative Real.java %}
 ```