JML Reference Manual 2013

User Manual:

Open the PDF directly: View PDF .
Page Count: 209 [warning: Documents this large are best viewed by clicking the View PDF Link!]

Scroll down to view the document on your mobile browser.

Introduction
- Behavioral Interface Specifications
- A First Example
- What is JML Good For?
- Status and Plans for JML
- Historical Precedents
- Acknowledgments
Fundamental Concepts
- Types can be Classes and Interfaces
- Model and Ghost
- Lightweight and Heavyweight Specifications
- Privacy Modifiers and Visibility
- Instance vs. Static
- Locations and Aliasing
- Expression Evaluation and Undefinedness
- Null is Not the Default
- Language Levels
Syntax Notation
Lexical Conventions
- White Space
- Lexical Pragmas
- Comments
- Annotation Markers
- Documentation Comments
- Tokens
Compilation Units
- Package Declarations
- Import Declarations
Type Declarations
- Class and Interface Declarations
  - Subtyping for Type Declarations
  - Modifiers for Type Declarations
    - Pure Type Declarations
    - Model Type Declarations
- Modifiers
Class and Interface Member Declarations
- Java Member Declarations
  - Method and Constructor Declarations
  - Field and Variable Declarations
    - JML Modifiers for Fields
    - Type-Specs
- Class Initializer Declarations
Type Specifications
- Introductory ADT Specification Examples
- Invariants
- Constraints
- Represents Clauses
- Initially Clauses
- Axioms
- Readable If Clauses
- Writable If Clauses
- Monitors For Clause
Method Specifications
- Basic Concepts in Method Specification
- Organization of Method Specifications
- Access Control in Specification Cases
- Lightweight Specification Cases
- Heavyweight Specification Cases
- Behavior Specification Cases
- Normal Behavior Specification Cases
- Exceptional Behavior Specification Cases
  - Pragmatics of Exceptional Behavior Specifications Cases
- Method Specification Clauses
Data Groups
- Static Data Group Inclusions
- Dynamic Data Group Mappings
Specification Inheritance
Predicates and Specification Expressions
- Predicates
- Specification Expressions
- Expressions
- JML Primary Expressions
- Set Comprehensions
- JML Operators
- Store Refs
Statements and Annotation Statements
- Local Declaration Statements
  - Modifiers for Local Declarations
- Loop Statements
  - Loop Invariants
  - Loop Variant Functions
- Assert Statements
- JML Annotation Statements
Redundancy
- Redundant Implications and Redundantly Clauses
- Redundant Examples
Model Programs
- Ideas Behind Model Programs
- Extracting Model Program Specifications
- Details of Model Programs
- Nondeterministic Choice Statement
- Nondeterministic If Statement
- Specification Statements
Specification for Subtypes
- Method of Specifying for Subclasses
- Code Contracts
Separate Files for Specifications
- File Name Suffixes
- Using Separate Files
- Type Checking Separate Files
- Default Constructors and Separate Files
Universe Type System
- Basic Concepts of Universes
- Rep and Peer
- Readonly
- Ownership Modifiers for Array Types
- Default Ownership Modifiers
- Ownership Type Rules
  - Ownership Subtyping
  - Ownership Typing for Expressions
- Casts and Ownership Types
Safe Math Extensions
- {@fam =@ttfam @def rm{tt}@tentt @backslashcurfont }bigint
- {@fam =@ttfam @def rm{tt}@tentt @backslashcurfont }real
Deprecated and Replaced Syntax
- Deprecated Syntax
- Replaced Syntax
Incompatible Changes
Grammar Summary
- Lexical Conventions
- Compilation Units
- Type Declarations
- Class and Interface Member Declarations
- Type Specifications
- Method Specifications
- Data Groups
- Specification Inheritance
- Predicates and Specification Expressions
- Statements and Annotation Statements
- Redundancy
- Model Programs
- Specification for Subtypes
- Separate Files for Specifications
- Universe Type System
- Safe Math Extensions
Modifier Summary
Type Checking Summary
Verification Logic Summary
Differences
- Differences Between JML and Other Tools
  - Differences Between JML and ESC/Java2
- Differences Between JML and Java
  - Non-null by Default
What's Missing
Bibliography
Index

Navigation menu