Editing

Author: davidcok

tutorial/FrameConditions.md

@@ -37,9 +37,9 @@ ensures clause that states that `counter2 == \old(counter2)`. This specification
 verifies as correct.
 
 But this is not a practical solution. We can't add to `increment1()`'s specification a clause stating that every visible variable is unchanged.
-Instead we use a *frame condition* whose purpose is to state what memory
+Instead we use a *frame condition* whose purpose is to state which memory
 locations a method might have modified. There are a variety of names for
-the frame clause: traditionally it is `assignable`, but `assigns` is also permitted.
+the frame clause: traditionally it is `assignable`, but `assigns` and `writes` are also permitted.
 Note that `modifies` is also an
 (implemented) synonym, but in some tools it has a slightly different meaning,
 so its use is not recommended.
@@ -69,8 +69,7 @@ that is written to in the body of `m`.
 * `a[*]` for array expression `a` means all elements of that array
 * `a[i..j]` for expressions `a`, `i`, and `j` means the stated range of array elements, from `i` to `j` inclusive.
 
-If there is no frame condition at all, then a default is used, namely `assigns \everything;`--- which means exactly that: after a call of this method, any memory location in the state might have been written to and might be changed. It is very difficult to prove anything about a program that includes a call to a method with such a frame condition. Thus  
-*you must include a frame condition for any method that is called within a program*.
+If there is no frame condition at all, then a default is used, namely `assigns \everything;`--- which means exactly that: after a call of this method, any memory location in the state might have been written to and might be changed. It is very difficult to prove anything about a program that includes a call to a method with such a frame condition. Thus *you must include a frame condition for any method that is called within a program*.
 
 A shorthand way to say that a method `assigns \nothing;` is to designate it `pure`, as in
 ```
@@ -84,7 +83,7 @@ though there are a few other details to purity --- see the [lesson on pure](Meth
 There are two other points to know about frame conditions. First, where a frame condition clause includes expressions, such as the indices of array expressions, those expressions are evaluated in the pre-state, not the post-state.
 
 Second, a frame condition is a method specification clause like `requires` and `ensures`. A method specification may contain more than one such clause.
-However, note that each cluase is considered individually. That is, each clause
+However, note that each clause is considered individually. That is, each clause
 by itself lists the memory locations that may be written to by the method.
 As each frame condition clause must be valid on its own, the effect of multiple clauses is the same as one clause with the _intersection_ of the sets of locations given by the separate clauses.
 For example,
@@ -110,7 +109,7 @@ result of mutiple assigns clauses was the *union* of their contents, but that is
 not the case, for historical reasons. The advice is then to
 *have only one frame condition clause per specification (case)*, even if that
 means the clause has a long list. (All the method specifications in the
-tutorial lessons so far have just one specification case; an advanced lesson
+tutorial lessons so far have just one specification case; a subsequent lesson
 presents [multiple specification cases](MultipleBehaviors).)
 
 

tutorial/JavaErrorsAndExceptions.md

@@ -0,0 +1,5 @@
+---
+title: JML Tutorial - Java Errors and Exceptions
+___
+
+_To be written_

tutorial/MethodCalls.md

@@ -20,7 +20,7 @@ The callee, on the right, is a simple standalone method. When the method is
 verified, the logical engine
 * assumes its preconditions are true
 * symbolically represents the actions of the method body
-* asserts the postconditions---that is, proves the the postconditions logically follow from the preconditions and method body in every initial state allowed by the preconditions
+* asserts the postconditions---that is, proves that the postconditions logically follow from the preconditions and method body in every initial state allowed by the preconditions
 
 As for the caller, it also follows the same three steps. But how do we represent the call to `callee()`? We could inline the whole callee method, but that would
 become unwieldy, would not work for recursion, and is not modular.
@@ -42,7 +42,7 @@ The following code is a simple example of a two-method verification.
 ```
 
 The output on verifying is given next. Note that the openjml command includes
-the `-progress` option, so we receive quite a bit more output.
+the `--progress` option, so we receive quite a bit more output.
 
 ```
 {% include_relative T_CallerCallee.out %}
@@ -70,8 +70,8 @@ is reported as not verified.
 
 A few additional points might be helpful.
 
-Often one is working on the specifications for just one method and so one does not want to try to verify everything. You can specify the one method to run like this:  
-`openjml --esc --method=caller2 T_CallerCallee.java`
+Often one is working on the specifications for just one method and so one does not want to try to verify everything. 
+You can specify the one method to run like this:  `openjml --esc --method=caller2 T_CallerCallee.java`
 
 Secondly, the `--progress` option is useful to see the detail about what verified and what did not; it also puts out information as work is accomplished, so you can see what progress is being made in a long-running job. But you can also reduce the amount of output. For example, the default `--normal` option
 ```
@@ -85,7 +85,7 @@ which just shows any error messages.
 
 If you want you can hide all the output text and just observe the exit code:
 ```
-openjml -esc T_CallerCallee.java > /tmp/t; echo $?
+openjml --esc --quiet T_CallerCallee.java ; echo $?
 ```
 produces just
 ```

tutorial/MultipleBehaviors.md

@@ -21,6 +21,7 @@ There are a few points to note:
 * There is no order to the behaviors; they can be written in any order that is understandable.
 * Every behavior applies on its own and must hold by itself --- there is no if-then-else  among them. If a behavior's preconditions hold,
 then its postconditions must hold, independent of what any other behavior says.
+* The effective precondition for each behavior is the conjunction (with `&&`) of the preconditions for that behavior. The effective precondition for the combination of multiple behaviors is the disjunction (with `||`) of the effective preconditions of the individual behaviors. Consequently, at the point where such a method is called, at least one, but by no means necessarily all, of the behaviors must have an effective precondition that is true.
 
 In our example, if `a`, `b`, and `c` are all equal, then the precondiition (`requires` clause) of each of the three behaviors is true.
 So the postconditions of each of the behaviors must also be true.  Fortunately they all agree.
@@ -66,7 +67,7 @@ The normal and exceptional behaviors illustrated in the previous section are ver
 The `normal_behavior` heading implies that no exception is allowed (`signals false`); the `exceptional_behavior` heading says that normal termination is not allowed (`ensures false`).
 A behavior that is neither of these is a simple `behavior`, which is the default when there is no heading.
 
-One other point: any one of the behavior keywords needs a visibility keyword; almost always, as in the example above, the visibility is the same as the method. The absence of a visibility modifier means `package` visibility, just as the absence of a visibility modifier on the method declaration.
+One other point: any one of the behavior keywords needs a visibility keyword; almost always, as in the example above, the visibility is the same as the method. The absence of a visibility modifier means `package` visibility, just as the absence of a visibility modifier on the method declaration. However, if there is no specialized behavior keyword, then there is no place for the visibility keyword; in that cae, the visibility is the same as the visibility of the method.
 
 ## Summary of specification cases
 

tutorial/OldAndOrdering.md

@@ -4,11 +4,12 @@ title: JML Tutorial - Method Specifications: old clauses and clause ordering
 
 We have introduced a few kinds of method specification clauses so far. In fact there are many more, though most are not widely used:
 * Precondition clauses
+  * [`recommends`](Recommends)
   * [`requires`](Preconditions)
   * [`old`](#old-clause)
 * Frame conditions
   * `reads` (`accessible`)
-  * [`assignable` (`assigns`)](FrameConditions)
+  * [`assignable` (`assigns`, `writes`)](FrameConditions)
   * `captures`
   * `callable`
 * Postconditions
@@ -28,15 +29,15 @@ Some of these have been already discussed; others are discussed in later lessons
 There is no pre-defined order to the clauses within a single specification case (cf. a later lesson on [multiple specification cases](MultipleBehaviors)].
 However, a specification is much more readable if the clauses generally follow the order above, with preconditions first, then frame conditions, followed by postconditions.
 
-There is some meaning to the ordering within the precondition group and within the postcondition group: earlier clauses can set conditions that are needed for later clause to be well-defined. For example,
+There is some meaning to the ordering within the precondition group and within the postcondition group: earlier clauses can set conditions that are needed for later clause to be well-defined; but ordering only matters within the kinds of precondition clauses and separately for any `ensures` clauses. For example,
 ```
 {% include_relative T_order1.java %}
 ```
 yields
 ```
-T_order1.old
+{% include_relative T_order1.out %}
 ```
-The first requires clause might not be well-defined because `a` might be null. If we reverse the order of the clauses, then JML is content:
+The first requires clause might not be well-defined because `a` might be null. If we reverse the order of the clauses, then OpenJML is content:
 ```
 {% include_relative T_order2.java %}
 ```

tutorial/Postconditions.md

@@ -79,5 +79,10 @@ This value is referenced as `\result`. Like all JML keywords in expression, `\re
 ```
 {% include_relative T_ensures3.java %}
 ```
-
+Two final points:
+* The order of `ensures` clauses matters. The predicates of a sequence of `ensures` clauses are effectively conjoined together (with `&&`) to produce
+a single postcondition predicate. Consequently an earlier predicate can cause a later predicate to be [well-defined](WellDefinedExpressions).
+* In thinking about postconditions, be aware of the semantics of the `ensures` clause, namely,
+_if the method terminates normally (with an exception), then the given postcondition is true_.
+The converse, if the `ensures` predicate is true then the method terminates normally, is not the meaning and is not necessarily true.
 ## **[Postconditions Problem Set](https://www.openjml.org/tutorial/exercises/PostConEx.html)**

tutorial/SpecifyingExceptions.md

@@ -16,7 +16,7 @@ So we could write this trivial example:
 ```
 which verifies successfully. Note that the specification includes a second kind of clause, the `signals_only` clause.
 This clause specifies the kinds of exceptions that may be thrown from the method. 
-JML requires the specification to list `RuntimeException` even though Java does not require declaring `RuntimeException` in a throws clause
+JML requires the specification to list `RuntimeException`, even though Java does not require declaring `RuntimeException` in a throws clause,
 in order to make it explicitly clear what exceptions might be thrown.
 
 If we omit any exceptions, by saying `signals_only \nothing`, a verification failure results.
@@ -56,4 +56,25 @@ as it should. We can guard against an exception by requiring that the method alw
 ```
 which now verifies again.
 
+Postcondition clauses can be stated in any order; there is no meaning to one being before the other.
+Consider this example in which there are two kinds of exceptions thrown.
+```
+{% include_relative T_Exception4.java %}
+```
+In the second `signals` clause, the expression `a != null` is required; without it, the later expression
+`a[i]` is not [well-defined](WellDefinedExpressions). It is immaterial that there is a test for `a` being null
+in the other `signals` clause. Note that if there are no `signals` clauses, then OpenJML complains that
+some expected conditions cannot be proved, as shown in this example:
+```
+{% include_relative T_Exception4a.java %}
+```
+which gives this result
+```
+{% include_relative T_Exception4a.out %}
+```
+The three verification failure messages may occur in any order.
+This balance between verification failures and exception specifications is an
+advanced topic discussed [here](JavaErrorsAndExceptions).
+
+
 ## **[Specifying Exceptions Problem Set](https://www.openjml.org/tutorial/exercises/SpecifyingExceptionsEx.html)**

tutorial/T_Exception4.java

@@ -0,0 +1,16 @@
+// openjml --esc T_Exception4.java
+//@ nullable_by_default
+public class T_Exception4 {
+
+    public static class V {
+        public int value;
+    }
+
+    //@ ensures \result == a[i];
+    //@ signals (NullPointerException e) a == null;
+    //@ signals (IndexOutOfBoundsException e) a != null && (i < 0 || i >= a.length);
+    //@ signals_only Exception;
+    public int value(int[] a, int i) {
+        return a[i];
+    }
+}

tutorial/T_Exception4a.java

@@ -0,0 +1,13 @@
+// openjml --esc T_Exception4a.java
+//@ nullable_by_default
+public class T_Exception4a {
+
+    public static class V {
+        public int value;
+    }
+
+    //@ ensures \result == a[i];
+    public int value(int[] a, int i) {
+        return a[i];
+    }
+}

tutorial/T_Exception4a.out

@@ -0,0 +1,10 @@
+T_Exception4a.java:11: verify: The prover cannot establish an assertion (PossiblyTooLargeIndex) in method value
+        return a[i];
+                ^
+T_Exception4a.java:11: verify: The prover cannot establish an assertion (PossiblyNegativeIndex) in method value
+        return a[i];
+                ^
+T_Exception4a.java:11: verify: The prover cannot establish an assertion (PossiblyNullDeReference) in method value
+        return a[i];
+                ^
+3 verification failures