More editing

Author: davidcok

tutorial/AssertStatement.md

@@ -1,5 +1,5 @@
 ---
-title: JML Tutorial - Assert statements (assert
+title: JML Tutorial - Assert statements (assert and check)
 ---
 A JML *assert* statement states a condition that is expected to hold at a point
 within the body of a method. Such statements are not part of a method's interface 
@@ -55,4 +55,36 @@ produces similar output:
 {% include_relative T_assert3.out %}
 ```
 
+## Check statement
+
+The `check` statement (e.g. `check neg < 0;`) is similar to the `assert` statement.
+It also effects a test of whether the given predicate is always true.
+However, the two statements differ in their effect on the subsequent logic
+of the program:
+
+* A `check` statement tests the predicate but makes no assumption about whether the
+predicate is subsequently true or false. A `check` statement essentially says,
+please just check whether the given predicate is true or false.
+* An `assert` predicate tests the predicate and then _assumes that it is subsequently true_.
+An `assert` statement essentially says, this predicate is supposed to be true, so pleasae test it
+and assume it to be true for analyzing subsequent code.
+
+For example,
+
+```
+{% include_relative T_assert4.java %}
+```
+
+produces this output:
+
+```
+{% include_relative T_assert4.out %}
+```
+
+This explanation points to a potentially confusing point about `assert` statements. If
+the given predicate is always false, then the implicit assumption, after the assert check,
+that it is true causes a complete halt to the symbolic execution -- there is no pre-state
+that satisfies the assert/assume combination. A `check` would be better to be used in such cases.
+
+
 ## **[Assert Statements Problem Set](https://www.openjml.org/tutorial/exercises/AssertEx.html)**

tutorial/Loops.md

@@ -70,7 +70,7 @@ Here is a typical for-each loop:
 {% include_relative  T_foreach.java %}
 ```
 Note that the (second) loop invariant states that so far (up to array index `\count`) all array elements are positive. That is because at the beginning of any loop iteration,
-all elements seen have been positive. As soon as a non-positive element is seen, the loop exists prematurely, but the verifier can follow this control flow to prove that 
+all elements seen have been positive. As soon as a non-positive element is seen, the loop exits prematurely, but the verifier can follow this control flow to prove that 
 the postcondition is valid for either exit.
 
 Note also the use of `\count` as a stand-in for a loop counter and the use of `\nothing` to say that nothing is modified in the loop body, other than `\count`, which is always included as a modified variable.

tutorial/SpecStatements.md

@@ -6,9 +6,13 @@ The basic unit of specification and verification in JML is the method,
 with the method body being compared to the method's specification.
 However, sometimes specifications within the body of a method can
 assist or are required to be able to prove that the body meets the
-method specification.
+method specification, and they can also be helpful in documenting
+a method body in a machine-checkable way.
+Such specification statements are not, however,
+part of the method's specification -- for example, they are not visible to 
+calling methods.
 
 The most common such specification statements are `assert`, `assume`,
 and `ghost` declaration statements. In addition, loops in a method
 body require a loop specification to be able to reason about the
-effect of that method body.s
+effect of that method body.

tutorial/T_assert4.java

@@ -0,0 +1,17 @@
+// openjml --esc T_assert4.java
+
+public class T_assert4 {
+  public int f;
+
+  public void example(/*@ nullable */ T_assert4 t) {
+    //@ check t != null; // ERROR, because not necessarily so
+    int k = t.f; // ERROR because t might be null
+  }
+
+  public void example2(/*@ nullable */ T_assert4 t) {
+    //@ assert t != null; // ERROR, because not necessarily so
+                          // but subsequently assumes it is true
+    int k = t.f; // OK
+  }
+
+}

tutorial/T_assert4.out

@@ -0,0 +1,10 @@
+T_assert4.java:8: verify: The prover cannot establish an assertion (PossiblyNullDeReference) in method example
+    int k = t.f; // ERROR because t might be null
+             ^
+T_assert4.java:7: verify: The prover cannot establish an assertion (Assert) in method example
+    //@ check t != null; // ERROR, because not necessarily so
+        ^
+T_assert4.java:12: verify: The prover cannot establish an assertion (Assert) in method example2
+    //@ assert t != null; // ERROR, because not necessarily so
+        ^
+3 verification failures