More editing

Author: davidcok

tutorial/Execution.md

@@ -25,6 +25,8 @@ The details of all the options are given in the [OpenJML Users' Guide](../docume
 
 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).
 
+A simple, example command-line is `openjml --esc --progress A.java` .
+
 ## Exit codes
 
 The executable returns with one of these exit values:

tutorial/SpecStatements.md

@@ -0,0 +1,14 @@
+---
+title: Specifications in Method Bodies
+---
+
+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.
+
+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

tutorial/Syntax.md

@@ -93,7 +93,7 @@ if
 So positive keys enable a comment and negative keys disable it, with any
 negative key overriding any positive ones.
 
-For example, a comment beginning `//-RAC@` will be used for typechecking (`--check`) and static checking (`--esc`), but ignored for runtime checking (`--rac`). A comment beginning `//+ESC@` will only be used when `-esc` is being applied.
+For example, a comment beginning `//-RAC@` will be used for typechecking (`--check`) and static checking (`--esc`), but ignored for runtime checking (`--rac`). A comment beginning `//+ESC@` will only be used when `--esc` is being applied.
 The most common use of conditional JML annotations is the first example: to turn off 
 non-executable annotations during runtime-assertion checking but leave
 them in place for static checking.

tutorial/index.md

@@ -44,22 +44,24 @@ example code; just add the appropriate path to the `openjml` command.
 * Simple Method Specifications
   * [Postconditions](Postconditions)
   * [Preconditions](Preconditions)
-  * [Assert statements](AssertStatement)
-  * [Assume statements](AssumeStatement)
-  * [JML Expressions](Expressions)
-  * [Well-defined Expressions](WellDefinedExpressions)
+  * [Specifying Exceptions](SpecifyingExceptions)
+  * [Method Specifications: old clauses and clause ordering](OldAndOrdering)
+  * [Multiple Method Behaviors](MultipleBehaviors)
+  * [Minimizing replicated specifications --- initially, constraint, invariant clauses](InitiallyConstraint)
   * [Verifying Method Calls](MethodCalls)
   * [Frame Conditions](FrameConditions)
   * [Specifying Constructors](Constructors)
   * [Using Method Calls in Specifications](MethodsInSpecifications)
+  * [Visibility](Visibility)
+* JML Expressions
+  * [JML Expressions](Expressions)
+  * [Well-defined Expressions](WellDefinedExpressions)
   * [Arithmetic](ArithmeticModes)
   * [Null and non-null](Nullness)
-  * [Visibility](Visibility)
+* [Method Body Specifications](SpecStatements)
+  * [Assert statements](AssertStatement)
+  * [Assume statements](AssumeStatement)
   * [Specifying Loops](Loops)
-  * [Specifying Exceptions](SpecifyingExceptions)
-  * [Method Specifications: old clauses and clause ordering](OldAndOrdering)
-  * [Multiple Method Behaviors](MultipleBehaviors)
-  * [Minimizing replicated specifications --- initially, constraint, invariant clauses](InitiallyConstraint)
   * [Ghost variables and computations](Ghost)
 
 * Inheritance