Minor edits

Author: davidcok

tutorial/Execution.md

@@ -13,14 +13,14 @@ or paths relative to the current working directory
 * 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) 
-(for OpenJML options, but only some Java option) use the syntax `-option=value`.
+(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.
 
 The details of all the options are given in the [OpenJML Users' Guide](../documentation/OpenJMLUserGuide.pdf). A few are worth mentioning here:
 * `--help` or `-?`: emit help information (about all of the options)
 * `--esc`: run static checking (the default is just parse and type-checking)
-* `--rac`: run runtime-assertion-checking
+* `--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).

tutorial/Installation.md

@@ -4,12 +4,12 @@ title: JML Tutorial - Installation
 
 Installation of OpenJML is simple:
 
-* Download the current release (in the 17.* or higher series, not the 8.* series) from [here](https://github.com/OpenJML/OpenJML/releases/latest)
+* Download the current release (in the 21.* or higher series) from [here](https://github.com/OpenJML/OpenJML/releases/latest).
 * Unzip the downloaded .zip file in a clean folder. The location and name of the directory are up to the user (though spaces in the folder name or path are not permitted).
 * The executable is the script named `openjml` in the top-level of the 
 installation. Do not move or rename this file, but you may make a link to the
 file or place it on your system PATH.
-* On a mac you may need to run `mac-setup` to enable permissions for the downloaded executables. You may also need to install `realpath` (for example, using `brew install coreutils`), so that symbolic links can be resolved (you only need this if you make a symbolic link to openjml or other executables in the installation.)
+* On a Mac you may need to run `mac-setup` to enable permissions for the downloaded executables. You may also need to install `realpath` (for example, using `brew install coreutils`), so that symbolic links can be resolved (you only need this if you make a symbolic link to openjml or other executables in the installation.)
 * OpenJML is a modified version of the OpenJDK `javac`. It is a standalone, 
 encapsulated executable; no installation of Java is needed to run it.
 

tutorial/Introduction.md

@@ -11,7 +11,7 @@ We know you are eager to just try out some code, but here is a quick set of bull
 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)
 * So when the method verifications are successful, the result is a more powerful statement of correctness than is testing/RAC
-* Each method is checked on its own, using the specifications (not the implementations) of the other methods.
+* Each method is checked on its own, using the specifications (not the implementations) of the other methods
 * This is a valid approach so long as, eventually, all methods verify successfully (and it can be proved that the program terminates)
 
 The tutorial walks you through basic JML, with plenty of examples that you can execute using OpenJML.

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.