More tutorial example editing

Author: davidcok

tutorial/Loops.md

@@ -50,15 +50,16 @@ It may help to understand what the verifier tries to prove about a loop. It prov
   * and does the update step
   * and the result must satisfy the loop invariants again (with the updated value of the loop index)
   * and also the termination expression must have decreased
-* Third, it assumes the first two steps above but that the loop condition is false and goes on to reason about any program steps and postconditions that follow the loop.
+* Third, it assumes the first two steps above and that the loop condition is false, and then proves that the loop invariants still hold
 
 In the example above, the second proof obligation assumes `0 <= i <= a.length` and `\forall int k; 0 <= k < i; a[k] == k;` and
 `(i < a.length)`, and then applies `a[i]=i` and `i++`, and proves `\forall int k; 0 <= k < i'; a[k]==k`, where `i'` is the updated `i`.
 
 It also must prove that `a.length-i` is non-negative at the start of the loop body and that after the loop index update that value is greater  than
 the new value of the expression, namely `a.length-i'`.
 
-The third proof obligation assumes `0 <= i <= a.length` and `\forall int k; 0 <= k < i; a[k] == k;` and `!(i < a.length)`, from which it can prove the `assert` statement.
+The third proof obligation assumes `0 <= i <= a.length` and `\forall int k; 0 <= k < i; a[k] == k;` and `!(i < a.length)`; 
+the loop invariants are still true, trivailly and they in turn imply the truth of the `assert` statement.
 
 ## For-each loops
 
@@ -84,19 +85,11 @@ A while loop generally follows the same pattern as a traditional for loop. Here
 
 ## Do-while loops
 
-Do-while loops can be tricky to specify because they do not follow the same update-at-the-start of a loop pattern. Here is a simple example.
+Do-while loops can be tricky to specify because they do not follow the same update-at-the-start of a loop pattern. Also, the loop body is executed at least once, because the
+loop condition is not evaluated until the end of the loop body. Here is a simple example.
 ```
 {% include_relative  T_dowhile.java %}
 ```
-Here the order of assumptions is this:
-* assume the loop invariants
-* execute the body
-* do the loop test (which in this example incorporates the loop update)
-* check that the loop invariants still hold
-
-Because the loop update and test are at the end of the body, the initial loop invariant only reflects the possible values at the start of the loop; the final increment and exit from the loop happen without 
-checking the loop invariant again. So the loop invariant here is `0 <= i < 10`, not `0 <= i <= 10`.
-
 
 ## Loop verification errors
 
@@ -146,4 +139,9 @@ which produces
 {% include_relative  T_LoopNegativeError.out %}
 ```
 
+## Loop conditions with side effects
+
+Good programming style avoids loop conditions with side effects. Nevertheless, such constructs are legal Java.
+However, writing workable specifications for such programs is tricky, reflecting the fact that understanding and writing correct programs using conditions with side-effects is tricky.
+
 ## **[Specifying Loops Problem Set](https://www.openjml.org/tutorial/exercises/SpecifyingLoopsEx.html)**

tutorial/SpecStatements.md

@@ -1,5 +1,5 @@
 ---
-title: Specifications in Method Bodies
+title: JML Tutorial - Specifications in Method Bodies
 ---
 
 The basic unit of specification and verification in JML is the method,

tutorial/T_dowhile.java

@@ -4,14 +4,15 @@ public class T_dowhile {
   //@ requires 20 < a.length;
   public void test(int[] a) {
     int i = 0;
+    //@ maintaining i == \count;
     //@ maintaining 0 <= i <= 10;
-    //@ maintaining i == \count && (\count > 0 ==> i < 10);
     //@ maintaining \forall int k; 0 <= k < i; a[k] == 0;
     //@ loop_writes i, a[*];
     //@ decreases 10-i;
     do {
       a[i] = 0;
-    } while (++i < 10);
+      ++i;
+    } while (i < 10);
     //@ assert \forall int k; 0 <= k < 10; a[k] == 0;
   }
 }

tutorial/T_foreach.java

@@ -7,8 +7,8 @@ public boolean allPositive(int[] a) {
     //@ maintaining \forall int k; 0 <= k < \count; a[k] > 0;
     //@ loop_writes \nothing;
     //@ decreases a.length - \count;
-    for (int i: a) {
-      if (i <= 0) return false;
+    for (int v: a) {
+      if (v <= 0) return false;
     }
     return true;
   }

tutorial/exercises/ArithmeticExample2.out

@@ -0,0 +1,4 @@
+ArithmeticExample2.java:9: verify: The prover cannot establish an assertion (ArithmeticOperationRange) in method updatePlayerHealth: overflow in int sum
+			return (playerHealth + dmg);
+			                     ^
+1 verification failure

tutorial/exercises/AssertExample2.out

@@ -0,0 +1,7 @@
+AssertExample2.java:22: verify: The prover cannot establish an assertion (Postcondition: AssertExample2.java:4:) in method primeChecker
+		return isPrime;
+		^
+AssertExample2.java:4: verify: Associated declaration: AssertExample2.java:22:
+	//@ ensures \result <==> !(\exists int i; i >= 2; num % i == 0);
+	    ^
+2 verification failures

tutorial/exercises/CallingMethodsExample1.out

@@ -0,0 +1,4 @@
+CallingMethodsExample1.java:40: verify: The prover cannot establish an assertion (Assert) in method testClass
+		//@ assert isClassFailing(classGrades);
+		    ^
+1 verification failure

tutorial/exercises/CallingMethodsExample2.out

@@ -0,0 +1,8 @@
+CallingMethodsExample2.java:42: warning: A non-pure method is being called where it is not permitted: CallingMethodsExample2.isClassFailing(double[])
+		//@ assert isClassFailing(classGrades);
+		                         ^
+CallingMethodsExample2.java:42: verify: The prover cannot establish an assertion (Assert) in method testClass
+		//@ assert isClassFailing(classGrades);
+		    ^
+1 warning
+1 verification failure

tutorial/exercises/MethodCallsExample2.out

@@ -0,0 +1,4 @@
+MethodCallsExample2.java:14: verify: The prover cannot establish an assertion (Assert) in method enoughMaterial
+		//@ assert (area > materialSqFt);
+		    ^
+1 verification failure

tutorial/exercises/SpecifyingExceptionsExample2.out

@@ -0,0 +1,6 @@
+SpecifyingExceptionsExample2.java:10: error: cannot find symbol
+    @   ensures \result == str.length % tableSize; 
+                              ^
+  symbol:   variable length
+  location: variable str of type String
+1 error