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

---

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html