Table of Contents

1. 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

2. 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

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

3. Syntax Notation
4. Lexical Conventions

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

5. Compilation Units

5.1 Package Definitions
5.2 Import Definitions

6. Type Definitions

6.1 Class and Interface Definitions

6.1.1 Subtyping for Type Definitions
6.1.2 Modifiers for Type Definitions

6.2 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

7. Class and Interface Member Declarations

7.1 Java Member Declarations

7.1.1 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

7.1.2 Field and Variable Declarations

7.1.2.1 JML Modifiers for Fields
7.1.2.2 Type-Specs

7.2 Class Initializer Declarations

8. Type Specifications

8.1 Introductory ADT Specification Examples
8.2 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

8.3 Constraints

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

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

9. 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.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

9.7 Normal Behavior Specification Cases
9.8 Exceptional Behavior Specification Cases

9.8.1 Pragmatics of Exceptional Behavior Specifications Cases

9.9 Method Specification Clauses

9.9.1 Specification Variable Declarations

9.9.1.1 Forall Variable Declarations
9.9.1.2 Old 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

10. Data Groups

10.1 Static Data Group Inclusions
10.2 Dynamic Data Group Mappings

11. Predicates and Specification Expressions

11.1 Predicates
11.2 Specification Expressions
11.3 Expressions
11.4 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

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

11.5 Set Comprehensions
11.6 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

11.7 Store Refs

12. Statements and Annotation Statements

12.1 Local Declaration Statements

12.1.1 Modifiers for Local Declarations

12.2 Loop Statements

12.2.1 Loop Invariants
12.2.2 Loop Variant Functions

12.3 Assert Statements
12.4 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

13. Redundancy

13.1 Redundant Implications and Redundantly Clauses
13.2 Redundant Examples

14. 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

14.6.1 Continues Clause
14.6.2 Breaks Clause
14.6.3 Returns Clause

15. Specification for Subtypes

15.1 Method of Specifying for Subclasses
15.2 Code Contracts

16. Refinement

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

16.5.1 Default Constructor Refinement

17. MultiJava Extensions to JML

17.1 Augmenting Method Declarations
17.2 MultiMethods

18. 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.6.1 Ownership Subtyping
18.6.2 Ownership Typing for Expressions

18.7 Casts and Ownership Types

19. Safe Math Extensions

19.1 \bigint
19.2 \real

20. Deprecated and Replaced Syntax

20.1 Deprecated Syntax
20.2 Replaced Syntax

A. Grammar Summary

A.1 Lexical Conventions
A.2 Compilation Units
A.3 Type Definitions
A.4 Class and Interface Member Declarations
A.5 Type Specifications
A.6 Method Specifications
A.7 Data Groups
A.8 Predicates and Specification Expressions
A.9 Statements and Annotation Statements
A.10 Redundancy
A.11 Model Programs
A.12 Specification for Subtypes
A.13 Refinement
A.14 MultiJava Extensions to JML
A.15 Universe Type System
A.16 Safe Math Extensions
A.17 Deprecated and Replaced Syntax

B. Modifier Summary
C. Type Checking Summary
D. Verification Logic Summary
E. Differences

E.1 Differences Between JML and Other Tools

E.1.1 Differences Between JML and ESC/Java2

E.2 Differences Between JML and Java

E.2.1 Non-null by Default

F. What's Missing
Bibliography
Index