Editing

Author: davidcok

tutorial/ArithmeticModes.md

@@ -31,7 +31,7 @@ as mathematical---that is, that specifications use infinite precision arithmetic
 Consequently, JML defines three *arithmetic modes* (for integer arithmetic):
 
 * Java mode: arithmetic behaves precisely as in Java, with silent wrap-around of overflowing and underflowing operations
-* Safe mode: the results of arithmetic operations are the same as in Java mode, but verification errors are issued if the operation may overflow
+* Safe mode: the results of arithmetic operations are the same as in Java mode, but verification errors are issued if the operation may over/underflow
 * Math (bigint) mode: Values and operations are in mathematical arithmetic---values are unbounded and so there is no over/underflow.
 
 The default is *safe mode* for expressions in Java code and *math mode* for
@@ -83,10 +83,10 @@ specific arithmetic mode using the functions `\java_math(...)`, `\safe_math(...)
 These each take one argument and return the value of the argument, but the
 argument expression is computed using the given mode. These operations are
 not available for Java code, because there are no such operations in Java.
-* The mode for a proof attempt using OpenJML can be set using command-line options: `-code-math=...` and `-spec-math=...` to set the mode for Java code and specifications, respectively, with possible values of `java`, `safe`, and `bigint`.
-For example, to turn off overflow warnings in the Java code one can set the global default using `-code-math=java`
+* The mode for a proof attempt using OpenJML can be set using command-line options: `--code-math=...` and `--spec-math=...` to set the mode for Java code and specifications, respectively, with possible values of `java`, `safe`, and `bigint`.
+For example, to turn off overflow warnings in the Java code one can set the global default using `--code-math=java`
 * You can set the mode for a particular method using the modifiers
-`code_java_math`, `spec_java_math`, `code_safe_math`, `spec_safe_math` and `spec_bigint_math` (`code-bigint-math` is not an operational mode at present).
+`code_java_math`, `spec_java_math`, `code_safe_math`, `spec_safe_math` and `spec_bigint_math` (`code_bigint_math` is not an operational mode at present).
 In this example, both the code and specs are computed with java math, so they agree, even when there is an overflow.
 
 ```

tutorial/T_show4.check

@@ -0,0 +1,2 @@
+( openjml --esc T_show4.java )  2>&1 | diff - T_show4.out
+echo "T_show4.check is nondeterministic -- check it by hand"

tutorial/Visibility.md

@@ -38,7 +38,7 @@ obviates the goal of having hidden an implementation in the first place. If an
 implementation is hidden in private declarations, exposed to a client only through
 public methods, then we need a specification idiom that respects that.
 
-That is one purpose of model fields, which are preented in the [next lesson](ModelFields).
+That is one purpose of model fields, which are presented in a [subsequent lesson](ModelFields).
 But here we'll repeat our example using a model field.
 
 ```

tutorial/WellDefinedExpressions.md

@@ -30,7 +30,7 @@ The rules for well-definedness of a JML expression build up from the leaves of t
 * `a.length` is well-defined if `a` is well-defined and not null
 * `a[i]` is well-defined if expressions `a` and `i` are well-defined, `a` is not null, and `0 <= i < a.length`
 * all unary and binary operator expressions (excluding `&&` and `||` and `==>`)
- are well-defined if (a) the operands are well-defined, (b) for division (`/`) and modulo (`%`), the right operand is not zero, (c) the result of the operation is in range of the result type (depending on the [arithmetic mode](ArithmeticModes), and (d) for bit-shift operations (`<<`, `>>`, '>>>`), the value is the right operand is non-negative and less than the number of bits in the type of the left operand
+ are well-defined if (a) the operands are well-defined, (b) for division (`/`) and modulo (`%`), the right operand is not zero, (c) the result of the operation is in range of the result type (depending on the [arithmetic mode](ArithmeticModes)), and (d) for bit-shift operations (`<<`, `>>`, `>>>`), the value of the right operand is non-negative and less than the number of bits in the type of the left operand
 * the short-circuiting `&&` is well-defined if the left operand is well-defined and, if the left operand is true, the right operand is well-defined
 * the short-circuiting `||` is well-defined if the left operand is well-defined and, if the left operand is false, the right operand is well-defined
 * a `==>`  expression is well-defined if the left operand is well-defined and,