Merge branch 'master' of https://github.com/OpenJML/openjml.github.io

Author: davidcok

documentation/JML_Reference_Manual.pdf

@@ -4,15 +4,15 @@
 public class SelectionSort {    
     /*@
         assigns arr[*];
-        ensures \forall int k;0 <= k && k < arr.length-1;arr[k] >= arr[k+1];
+        ensures \forall int k; 0 <= k && k < arr.length-1; arr[k] >= arr[k+1];
     @*/
+    // Sorts the array in-place from maximum down to minimum
     public static void sort(int /*@ non_null @*/ [] arr) {
         //@ ghost final int n = arr.length;
 
         //@ loop_invariant 0 <= i <= n; // Bounds check
-        /*@ loop_invariant \forall int j; 0 <= j < i; // Sorted up-to i
-                               \forall int k; j < k < n; arr[j] >= arr[k];
-        @*/
+        //@ loop_invariant \forall int j; 0 <= j < i; // Sorted up-to i
+        //@                    \forall int k; j < k < n; arr[j] >= arr[k];
         //@ loop_assigns i, arr[*];
         //@ decreasing n-i; // i goes up
         for (int i = 0; i < arr.length; i++) {
@@ -24,7 +24,7 @@ public static void sort(int /*@ non_null @*/ [] arr) {
 
             //@ loop_invariant i < j <= n; // Bounds check
             //@ loop_invariant \forall int k; i <= k < j; ub >= arr[k]; // max elem up-to j
-            //@ loop_invariant i <= l < n; // max index bounds check
+            //@ loop_invariant i <= l < j; // max index bounds check
             //@ loop_invariant ub == arr[l]; // max index corresponds to max elem.
             //@ loop_assigns j, l, ub;
             //@ decreasing n-j; // j goes up
@@ -36,9 +36,6 @@ public static void sort(int /*@ non_null @*/ [] arr) {
             }
             // Maximum is at position l
 
-            // assert \forall int k; 0 <= k < i; largest <= arr[k];
-            // assert \forall int k; i <= k < n; largest >= arr[k];
-            
             arr[l] = arr[i];
             arr[i] = ub;
         }

documentation/OpenJMLUserGuide.pdf

@@ -4,15 +4,15 @@ title: JML Tutorial - Executing openjml
 
 ## Options and files
 
-The `openjml` executable is a modified version of the OpenJDK `javac`
+The `openjml` executable is a modified version of the OpenJDK compiler `javac`
 and is correspondingly a classic command-line tool:
 * The command-line arguments are a mix of files and options.
 * Files are given as absolute file paths 
 or paths relative to the current working directory
 (not relative to the location of `openjml`).
 * Options inherited from `javac` are unchanged. They are a mix of single-hyphen and double-hyphen spellings.
 * OpenJML-specific options begin with a double hyphen (e.g., `--quiet`) (single hyphens are still accepted for most options). 
-Options that take a value either (a) have the value follow the option as the next argument or (b) 
+Options that take a value either: (a) have the value follow the option as the next argument or (b) 
 (for OpenJML options, but only some Java option) use the syntax `--option=value`.
 For some options, the value may be a comma-separated list; if the value contains
 whitespace, it must be enclosed in quotes.
@@ -23,7 +23,7 @@ The details of all the options are given in the [OpenJML Users' Guide](../docume
 * `--rac`: compile with embedded checks, for runtime-assertion-checking
 * `--progress`: emits more information during processing than the default `--normal`
 
-Use `--class-path` or `-cp` just as you would for `javac` to specify the list of folders on which to find files. `openjml` uses a classpath and a sourcepath exactly like `javac` does; in addition `openjml` considers a _specspath_ for finding specification files. For most applications, it is simplest to define a single classpath (using the `-cp` command-line option or the `CLASSPATH` environment variable) giving the jar files and folder roots of package hierarchies for all the class, source and specification files. The details are an advanced topic presented [here](SpecificationFiles).
+Use `--class-path` or `-cp` just as you would for `javac` (i.e., with a path argument after a space, such as `-cp '/home/me/project1:/home/me/prjoject2'`) to specify the list of folders on which to find files. `openjml` uses a classpath and a sourcepath exactly like `javac` does; in addition `openjml` also uses a _specspath_ for finding specification files. For most applications, it is simplest to define a single classpath (using the `-cp` command-line option or the `CLASSPATH` environment variable) giving the jar files and folder roots of package hierarchies for all the class, source and specification files. The details are an advanced topic presented [here](SpecificationFiles).
 
 A simple, example command-line is `openjml --esc --progress A.java` .
 

examples/SelectionSort.java

@@ -20,7 +20,7 @@ in the pre-state, that is, the state at the beginning of the method's execution.
 `counter1` without the `\old` designator means the value of `counter1` in the
 post-state, the state after the method has completed.
 
-Also, why the comparison to `Integer.MAX_VALUE`? That is to avoid warnings about arithmetic overflow. We'll get to that topic [later](ArithmeticModes).
+Also, why the comparison to `Integer.MAX_VALUE` in the preconditions? That is to avoid warnings about arithmetic overflow. We'll get to that topic [later](ArithmeticModes).
 
 Now to the point of this lesson. The two increment methods verify, but 
 what is happening in the test method?
@@ -36,7 +36,7 @@ that `counter2` is unchanged. One solution would be to add an additional
 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.
+But adding such postconditions 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 which memory
 locations a method might have modified. There are a variety of names for
 the frame clause: traditionally it is `assignable`, but `assigns` and `writes` are also permitted.
@@ -70,12 +70,12 @@ program state outside of the method.
 * The formal arguments of the method are in scope for the frame condition,
 just like for the `requires` and `ensures` clauses. The formal arguments 
 themselves cannot be changed by a method, but if they are references to objects,
-their fields might be written to by a method. So a method `m(MyType q)`
+then the fields of those objects might be written to by the method. So a method `m(MyType q)`
 might have a frame condition `assigns q.f;` if `f` is a field of `MyType`
 that is written to in the body of `m`.
 * If a method has no external effects other than its return value, you can specify a frame condition `assigns \nothing;`
 * `q.*` for an expression `q` means all fields of q
-* `a[i]` for expression `a` and `i` means that particular array element
+* `a[i]` for expressions `a` and `i` means the particular array element `a[i]` (where the values of `a` and `i` are interpreted in the method's pre-state)
 * `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.
 
@@ -88,7 +88,7 @@ public void m() { ... }
 ```
 though there are a few other details to purity --- see the [lesson on pure](MethodsInSpecifications).
 
-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.
+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. This allows callers of the method to understand the potential side-effects of the method before calling it.
 
 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 clause is considered individually. That is, each clause

examples/userguide-examples.zip

@@ -2,15 +2,15 @@
 title: JML Tutorial - Minimizing replicated specifications (initially, constraint, invariant clauses)
 ---
 
-Sometimes it is the case that certain properties must hold at the end of every constructor or every method.
-Then the specifications for each method or constructor have to repeat the same specification clause.
-There is a danger that (a) such a clause will be forgotten for some constructor or method and (b) if the clause needs to be modified, it will not be correctly changed in every place it appears.
+Sometimes certain properties must hold at the end of every constructor or every method.
+Then the specifications for each method or constructor would have to repeat the same specification clause in every constructor or method's specification.
+However, there is a danger that: (a) such a clause will be forgotten for some constructor or method and (b) if the clause needs to be modified, it will not be correctly changed in every place it appears.
 
-So JML has a few features to coalesce such replicated clauses. These clauses are part of the _class_ declaration, but apply to every method or constructor as described below.
+So JML has a few features to coalesce such replicated clauses. These clauses are part of the _class_ declaration, but apply to every method or constructor in the class (or interface) as described below.
 
 ## Initially clauses
 
-An `initially` clause at the class level is equivalent to a corresponding `ensures` clause at the end of every constructor, including an unwritten default constructor. For example, suppose we are constructing rectangles and want to ensure that, at least upon construction, every such rectangle has a length larger than its width, which is larger than 0.  We might write
+An `initially` clause at the class level is equivalent to a corresponding `ensures` clause at the end of every constructor, including any unwritten default constructor. For example, suppose we are constructing rectangles and want to ensure that, at least upon construction, every such rectangle has a length larger than its width, which is larger than 0.  We might write
 ```
 {% include_relative T_initially1.java %}
 ```
@@ -20,7 +20,7 @@ This yields
 ```
 This verification failure is understandable. We did not specify a precondition that `0 < width < length`, so the stated initially clause cannot be fulfilled.
 But why is there no failure for the second constructor? The second constructor calls `this(0,0)`, using the first constructor. Because it is calling that
-constructor, it only uses that constructor's specifications in reasoning about its own implementation. So the second constructor sees
+constructor, it only uses that constructor's specifications in reasoning about its own implementation. So the call of the first constructor by the second constructor sees
 ```
    assume \let width = 0 && length = 0 in (this.width == width && this.length == length) 
    assume 0 < this.width < this.length
@@ -32,13 +32,13 @@ If we insert a precondition to fix the verification of the first constructor, we
 ```
 {% include_relative T_initially2.java %}
 ```
-which yeilds
+which yields:
 ```
 {% include_relative T_initially2.out %}
 ```
 Now the first constructor passes verification, but the second one does not. The reason is obvious: 
-the size we have given for a default rectangle (0 by 0) does not satisfy our desired `initially` postcondition. 
-We'll have a to pick a different size -- 1x2 perhaps.
+the size we have given for a default rectangle (0 by 0) does not satisfy our desired `initially` postcondition, which was enforced by the new precondition on the first constructor.
+To fix this failure, we would have a to pick different sizes -- 1x2 perhaps.
 
 ## Constraint clauses
 

tutorial/Execution.md

@@ -2,11 +2,12 @@
 title: JML Tutorial - What is Deductive Verification?
 ---
 
-We know you are eager to just try out some code, but here is a quick set of bullet points to be sure you understand where this tutorial is headed:
-* JML is a language for writing specifications for Java programs
-* OpenJML is tool for checking that the Java implementation of the program is consistent with the JML specifications
-* This checking can either be done statically (without running the program) -- called Deductive Verification - DV or ESC (Extended static checking)
-* or it can be done by running test cases through an instrumented program (RAC - runtime-assertion-checking)
+We know you are eager to just try out some code, but here is a quick set of points to be sure you understand where this tutorial is headed:
+* JML is a language for writing specifications of the behavior of Java programs.
+* OpenJML is tool for checking that the Java implementation of the program is consistent with its JML specifications.
+* This checking can either be done:
+   * statically (without running the program) -- called Deductive Verification, - DV or ESC (Extended Static Checking), or
+   * dynamically by running test cases through an instrumented program - RAC (Runtime Assertion Checking).
 
 The tutorial is mostly focussed on DV/ESC (though there are lessons on RAC as well):
 * The DV approach is akin to logically symbolically executing a method for every possible legal set of inputs (every possible pre-state)

tutorial/FrameConditions.md

@@ -2,14 +2,16 @@
 title: JML Tutorial - Method Calls
 ---
 
-We have seen how to verify methods that have pre- and postconditions to describe
+We have seen how to verify method implementations that have
+pre- and postconditions describing
 the behavior of method bodies that contain if statements and assignments.
 Now let's progress to method calls.
 
 The key point to remember is that verification in JML (and other similar
 deductive verification languages and tools) is *modular by method*.
 That is, each method is verified on its own; only when all methods are 
-verified with a consistent set of specifications across all of them can the program as a whole be 
+verified with a consistent set of specifications
+across all of them can the program as a whole be 
 considered verified.
 
 Consider two methods, a caller and a callee, as shown in this diagram.
@@ -30,7 +32,7 @@ pre- and post-conditions. We know that the callee's postconditions will be true
 * must prove (assert) that the callee's preconditions hold
 * and then it may assume that the callee's postconditions will hold
 
-As long as we keep the callee's specifications the same, we can verify the callee and the caller independently.
+As long as we keep the callee's specifications the same, we can verify the callee and the caller independently. (Thus the callee's specification is a summary of its behavior and is not affected by the callee's implementation details.)
 
 It is easy to see that this process works for verifying the methods in a program that do not call anything, to those methods that just call those leaves, all the way up to the top-level methods of the program. It can also be demonstrated that this process is sound when there are recursive calls, as long as it can
 be proved that the program terminates.
@@ -51,7 +53,7 @@ the `--progress` option, so we receive quite a bit more output.
 Looking at this piece by piece:
 * The method `lessThanDouble` requires positive inputs with the first argument
 larger than the second. It returns true if the first argument is less than double the second. The method proves without a problem. 
-The output about `lessThanDouble` is near the end of the listing.
+The output about `lessThanDouble` is near the end of the verification listing above.
 * The default constructor `T_CallerCallee()` also verifies without problem.
 * The method `caller1` calls `lessThanDouble` for two test cases and checks 
 that the result is what is expected. This method also verifies.