JML Reference Manual

The Java Modeling Language (JML) is a notation for formally specifying the behavior and interfaces of Java classes and methods. The purpose of this manual is to precisely define JML's syntax and semantics.

1. Introduction
2. Fundamental Concepts
3. Syntax Notation
4. Lexical Conventions
5. Compilation Units
6. Type Declarations
7. Class and Interface Member Declarations
8. Type Specifications
9. Method Specifications
10. Data Groups
11. Specification Inheritance
12. Predicates and Specification Expressions
13. Statements and Annotation Statements
14. Redundancy
15. Model Programs
16. Specification for Subtypes
17. Separate Files for Specifications
18. Universe Type System
19. Safe Math Extensions
A. Deprecated and Replaced Syntax
B. Incompatible Changes
C. Grammar Summary
D. Modifier Summary
E. Type Checking Summary
F. Verification Logic Summary
G. Differences
Bibliography
Index

 -- The Detailed Node Listing ---

Introduction

1.1 Behavioral Interface Specifications
1.2 A First Example
1.3 What is JML Good For?
1.4 Status and Plans for JML
1.5 Historical Precedents
1.6 Acknowledgments

Fundamental Concepts

2.1 Types can be Classes and Interfaces
2.2 Model and Ghost
2.3 Lightweight and Heavyweight Specifications
2.4 Privacy Modifiers and Visibility
2.5 Instance vs. Static
2.6 Locations and Aliasing
2.7 Expression Evaluation and Undefinedness
2.8 Null is Not the Default
2.9 Language Levels

Language Levels

2.9.1 Level 0 Features
2.9.2 Level 1 Features
2.9.3 Level 2 Features
2.9.4 Level 3 Features
2.9.5 Level C Features
2.9.6 Level X Features

Lexical Conventions

4.1 White Space
4.2 Lexical Pragmas
4.3 Comments
4.4 Annotation Markers
4.5 Documentation Comments
4.6 Tokens

Compilation Units

5.1 Package Declarations
5.2 Import Declarations

Type Declarations

6.1 Class and Interface Declarations
6.2 Modifiers

Class and Interface Declarations

6.1.1 Subtyping for Type Declarations
6.1.2 Modifiers for Type Declarations

Modifiers for Type Declarations

6.1.2.1 Pure Type Declarations
6.1.2.2 Model Type Declarations

Modifiers

6.2.1 Suggested Modifier Ordering
6.2.2 Java Annotations
6.2.3 Spec Public
6.2.4 Spec Protected
6.2.5 Pure
6.2.6 Model
6.2.7 Ghost
6.2.8 Instance
6.2.9 Helper
6.2.10 Monitored
6.2.11 Uninitialized
6.2.12 Math Modifiers
6.2.13 Nullity Modifiers

Class and Interface Member Declarations

7.1 Java Member Declarations
7.2 Class Initializer Declarations

Java Member Declarations

7.1.1 Method and Constructor Declarations
7.1.2 Field and Variable Declarations

Method and Constructor Declarations

7.1.1.1 Formal Parameters
7.1.1.2 Model Methods and Constructors
7.1.1.3 Pure Methods and Constructors
7.1.1.4 Helper Methods and Constructors

Field and Variable Declarations

7.1.2.1 JML Modifiers for Fields
7.1.2.2 Type-Specs

Type Specifications

8.1 Introductory ADT Specification Examples
8.2 Invariants
8.3 Constraints
8.4 Represents Clauses
8.5 Initially Clauses
8.6 Axioms
8.7 Readable If Clauses
8.8 Writable If Clauses
8.9 Monitors For Clause

Invariants 

8.2.1 Static vs. instance invariants
8.2.2 Invariants and Exceptions
8.2.3 Access Modifiers for Invariants
8.2.4 Invariants and Inheritance

Constraints 

8.3.1 Static vs. instance constraints
8.3.2 Access Modifiers for Constraints
8.3.3 Constraints and Inheritance

Method Specifications

9.1 Basic Concepts in Method Specification
9.2 Organization of Method Specifications
9.3 Access Control in Specification Cases
9.4 Lightweight Specification Cases
9.5 Heavyweight Specification Cases
9.6 Behavior Specification Cases
9.7 Normal Behavior Specification Cases
9.8 Exceptional Behavior Specification Cases
9.9 Method Specification Clauses

Invariants and constraints 

9.6.1 Semantics of flat behavior specification cases
9.6.2 Semantics of non-helper methods
9.6.3 Semantics of non-helper constructors
9.6.4 Semantics of helper methods and constructors
9.6.5 Semantics of nested behavior specification cases

Exceptional Behavior Specification Cases

9.8.1 Pragmatics of Exceptional Behavior Specifications Cases

Method Specification Clauses

9.9.1 Specification Variable Declarations
9.9.2 Requires Clauses
9.9.3 Ensures Clauses
9.9.4 Signals Clauses
9.9.5 Signals-Only Clauses
9.9.6 Parameters in Postconditions
9.9.7 Diverges Clauses
9.9.8 When Clauses
9.9.9 Assignable Clauses
9.9.10 Accessible Clauses
9.9.11 Callable Clauses
9.9.12 Measured By Clauses
9.9.13 Captures Clauses
9.9.14 Working Space Clauses
9.9.15 Duration Clauses

Specification Variable Declarations

9.9.1.1 Forall Variable Declarations
9.9.1.2 Old Variable Declarations

Data Groups

10.1 Static Data Group Inclusions
10.2 Dynamic Data Group Mappings

Predicates and Specification Expressions

12.1 Predicates
12.2 Specification Expressions
12.3 Expressions
12.4 JML Primary Expressions
12.5 Set Comprehensions
12.6 JML Operators
12.7 Store Refs

JML Primary Expressions

12.4.1 \result
12.4.2 \old and \pre
12.4.3 \not_assigned
12.4.4 \not_modified
12.4.5 \only_accessed
12.4.6 \only_assigned
12.4.7 \only_called
12.4.8 \only_captured
12.4.9 \fresh
12.4.10 \reach
12.4.11 \duration
12.4.12 \space
12.4.13 \working_space
12.4.14 \nonnullelements
12.4.15 Informal Predicates
12.4.16 \typeof
12.4.17 \elemtype
12.4.18 \type
12.4.19 \lockset
12.4.20 \max
12.4.21 \is_initialized
12.4.22 \invariant_for
12.4.23 \lblneg and \lblpos
12.4.24 Quantified Expressions

Quantified Expressions

12.4.24.1 Universal and Existential Quantifiers
12.4.24.2 Generalized Quantifiers
12.4.24.3 Numerical Quantifier
12.4.24.4 Executability of Quantified Expressions
12.4.24.5 Modifiers for Bound Variables
12.4.24.6 Quantifying over Reference Types

JML Operators

12.6.1 Subtype operator
12.6.2 Equivalence and Inequivalence Operators
12.6.3 Forward and Reverse Implication Operators
12.6.4 Lockset Ordering

Statements and Annotation Statements

13.1 Local Declaration Statements
13.2 Loop Statements
13.3 Assert Statements
13.4 JML Annotation Statements

Local Declaration Statements

13.1.1 Modifiers for Local Declarations

Loop Statements

13.2.1 Loop Invariants
13.2.2 Loop Variant Functions

JML Annotation Statements

13.4.1 Assume Statements
13.4.2 Set Statements
13.4.3 Refining Statements
13.4.4 Unreachable Statements
13.4.5 Debug Statements
13.4.6 Hence By Statements

Redundancy

14.1 Redundant Implications and Redundantly Clauses
14.2 Redundant Examples

Model Programs

15.1 Ideas Behind Model Programs
15.2 Extracting Model Program Specifications
15.3 Details of Model Programs
15.4 Nondeterministic Choice Statement
15.5 Nondeterministic If Statement
15.6 Specification Statements

Specification Statements

15.6.1 Continues Clause
15.6.2 Breaks Clause
15.6.3 Returns Clause

Specification for Subtypes

16.1 Method of Specifying for Subclasses
16.2 Code Contracts

Separate Files for Specifications

17.1 File Name Suffixes
17.2 Using Separate Files
17.3 Type Checking Separate Files
17.4 Default Constructors and Separate Files

Universe Type System

18.1 Basic Concepts of Universes
18.2 Rep and Peer
18.3 Readonly
18.4 Ownership Modifiers for Array Types
18.5 Default Ownership Modifiers
18.6 Ownership Type Rules
18.7 Casts and Ownership Types

Ownership Type Rules

18.6.1 Ownership Subtyping
18.6.2 Ownership Typing for Expressions

Safe Math Extensions

19.1 \bigint
19.2 \real

Deprecated and Replaced Syntax

A.1 Deprecated Syntax
A.2 Replaced Syntax

Deprecated Syntax

A.1.1 Deprecated Annotation Markers
A.1.2 Deprecated Represents Clause Syntax
A.1.3 Deprecated Monitors For Clause Syntax
A.1.4 Deprecated File Name Suffixes
A.1.5 Deprecated Refine Prefix

Differences

G.1 Differences Between JML and Other Tools
G.2 Differences Between JML and Java

Differences Between JML and Other Tools

G.1.1 Differences Between JML and ESC/Java2

Differences Between JML and Java

G.2.1 Non-null by Default