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 Definitions
7. Class and Interface Member Declarations
8. Type Specifications
9. Method Specifications
10. Data Groups
11. Predicates and Specification Expressions
12. Statements and Annotation Statements
13. Redundancy
14. Model Programs
15. Specification for Subtypes
16. Refinement
17. MultiJava Extensions to JML
18. Universe Type System
19. Safe Math Extensions
20. Deprecated and Replaced Syntax
A. Grammar Summary
B. Modifier Summary
C. Type Checking Summary
D. Verification Logic Summary
E. 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 Definitions
5.2 Import Definitions

Type Definitions

6.1 Class and Interface Definitions
6.2 Modifiers

Class and Interface Definitions

6.1.1 Subtyping for Type Definitions
6.1.2 Modifiers for Type Definitions

Modifiers

6.2.1 Suggested Modifier Ordering
6.2.2 Spec Public
6.2.3 Spec Protected
6.2.4 Pure
6.2.5 Model
6.2.6 Ghost
6.2.7 Instance
6.2.8 Helper
6.2.9 Monitored
6.2.10 Uninitialized
6.2.11 Math Modifiers
6.2.12 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 Non-helper methods
9.6.3 Non-helper constructors
9.6.4 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

11.1 Predicates
11.2 Specification Expressions
11.3 Expressions
11.4 JML Primary Expressions
11.5 Set Comprehensions
11.6 JML Operators
11.7 Store Refs

JML Primary Expressions

11.4.1 \result
11.4.2 \old and \pre
11.4.3 \not_assigned
11.4.4 \not_modified
11.4.5 \only_accessed
11.4.6 \only_assigned
11.4.7 \only_called
11.4.8 \only_captured
11.4.9 \fresh
11.4.10 \reach
11.4.11 \duration
11.4.12 \space
11.4.13 \working_space
11.4.14 \nonnullelements
11.4.15 Informal Predicates
11.4.16 \typeof
11.4.17 \elemtype
11.4.18 \type
11.4.19 \lockset
11.4.20 \max
11.4.21 \is_initialized
11.4.22 \invariant_for
11.4.23 \lblneg and \lblpos
11.4.24 Quantified Expressions

Quantified Expressions

11.4.24.1 Universal and Existential Quantifiers
11.4.24.2 Generalized Quantifiers
11.4.24.3 Numerical Quantifier
11.4.24.4 Executability of Quantified Expressions
11.4.24.5 Modifiers for Bound Variables
11.4.24.6 Quantifying over Reference Types

JML Operators

11.6.1 Subtype operator
11.6.2 Equivalence and Inequivalence Operators
11.6.3 Forward and Reverse Implication Operators
11.6.4 Lockset Ordering

Statements and Annotation Statements

12.1 Local Declaration Statements
12.2 Loop Statements
12.3 Assert Statements
12.4 JML Annotation Statements

Local Declaration Statements

12.1.1 Modifiers for Local Declarations

Loop Statements

12.2.1 Loop Invariants
12.2.2 Loop Variant Functions

JML Annotation Statements

12.4.1 Assume Statements
12.4.2 Set Statements
12.4.3 Refining Statements
12.4.4 Unreachable Statements
12.4.5 Debug Statements
12.4.6 Hence By Statements

Redundancy

13.1 Redundant Implications and Redundantly Clauses
13.2 Redundant Examples

Model Programs

14.1 Ideas Behind Model Programs
14.2 Extracting Model Program Specifications
14.3 Details of Model Programs
14.4 Nondeterministic Choice Statement
14.5 Nondeterministic If Statement
14.6 Specification Statements

Specification Statements

14.6.1 Continues Clause
14.6.2 Breaks Clause
14.6.3 Returns Clause

Specification for Subtypes

15.1 Method of Specifying for Subclasses
15.2 Code Contracts

Refinement

16.1 File Name Suffixes
16.2 Using Separate Files
16.3 Refinement Chains
16.4 Type Checking Refinements
16.5 Refinement Viewpoints

Refinement Viewpoints

16.5.1 Default Constructor Refinement

MultiJava Extensions to JML

17.1 Augmenting Method Declarations
17.2 MultiMethods

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

20.1 Deprecated Syntax
20.2 Replaced Syntax

Differences

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

Differences Between JML and Other Tools

E.1.1 Differences Between JML and ESC/Java2

Differences Between JML and Java

E.2.1 Non-null by Default