Open JMLUser Guide
User Manual:
Open the PDF directly: View PDF
Page Count: 131 [warning: Documents this large are best viewed by clicking the View PDF Link!]
- Foreword
- Preface
- Introduction to specification and automatic checking
- Other resources
- I Tutorial
- II OpenJML User Guide
- Introduction to OpenJML
- OpenJML Concepts
- Running OpenJML as a command-line tool
- Running OpenJML
- OpenJML options
- Command-line options
- Options: JML tools
- The -no-internalSpecs option.
- Options: OpenJML options applicable to all OpenJML tools
- Options: Extended Static Checking
- Options: Runtime Assertion Checking
- Options: JML Information and debugging
- Java Options: Version of Java language or class files
- Java Options: Other Java compiler options applicable to OpenJML
- Java options related to annotation processing
- The Eclipse Plug-in
- Classpaths, sourcepaths, and specification paths in OpenJML
- OpenJML tools — Parsing and Type-checking
- OpenJML tools — Static Checking (ESC) and Verification
- Runtime Assertion Checking
- Static and Runtime warnings
- ArithmeticCastRange warning
- ArithmeticOperationRange warning
- Assert warning
- Assume warning (RAC only)
- Constraint warning
- Initially warning
- ExceptionalPostcondition warning
- PossiblyNegativeIndex warning
- PossiblyNegativeSize warning
- PossiblyTooLargeIndex warning
- Postcondition warning
- Precondition warning
- ExceptionalPostcondition warning
- Assignable warning
- Other OpenJML tools
- Limitations of OpenJML's implementation of JML
- Using OpenJML and OpenJDK within user programs
- Extending or modifying JML
- Contributing to OpenJML
- Installing OpenJML
- Installing the OpenJML Eclipse plug-in
- Static warning categories