JML Reference Manual: Table of Contents

[Top]

[Contents]

[Index]

[ ? ]

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 Declarations

5.2 Import Declarations

6. Type Declarations

6.1 Class and Interface Declarations

6.1.1 Subtyping for Type Declarations

6.1.2 Modifiers for Type Declarations

6.1.2.1 Pure Type Declarations

6.1.2.2 Model Type Declarations

6.2 Modifiers

6.2.1 Suggested Modifier Ordering

6.2.2 Java Annotations

6.2.12 Math Modifiers

6.2.13 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 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

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. Specification Inheritance

12. Predicates and Specification Expressions

12.1 Predicates

12.2 Specification Expressions

12.3 Expressions

12.4 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.13 \working_space

12.4.14 \nonnullelements

12.4.15 Informal Predicates

12.4.21 \is_initialized

12.4.22 \invariant_for

12.4.23 \lblneg and \lblpos

12.4.24 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

12.5 Set Comprehensions

12.6 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

12.7 Store Refs

13. Statements and Annotation Statements

13.1 Local Declaration Statements

13.1.1 Modifiers for Local Declarations

13.2 Loop Statements

13.2.1 Loop Invariants

13.2.2 Loop Variant Functions

13.3 Assert Statements

13.4 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

14. Redundancy

14.1 Redundant Implications and Redundantly Clauses

14.2 Redundant Examples

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

15.6.1 Continues Clause

15.6.2 Breaks Clause

15.6.3 Returns Clause

16. Specification for Subtypes

16.1 Method of Specifying for Subclasses

16.2 Code Contracts

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

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

A. Deprecated and Replaced Syntax

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

A.2 Replaced Syntax

B. Incompatible Changes

C. Grammar Summary

C.1 Lexical Conventions

C.2 Compilation Units

C.3 Type Declarations

C.4 Class and Interface Member Declarations

C.5 Type Specifications

C.6 Method Specifications

C.7 Data Groups

C.8 Specification Inheritance

C.9 Predicates and Specification Expressions

C.10 Statements and Annotation Statements

C.11 Redundancy

C.12 Model Programs

C.13 Specification for Subtypes

C.14 Separate Files for Specifications

C.15 Universe Type System

C.16 Safe Math Extensions

D. Modifier Summary

E. Type Checking Summary

F. Verification Logic Summary

G. Differences

G.1 Differences Between JML and Other Tools

G.1.1 Differences Between JML and ESC/Java2

G.2 Differences Between JML and Java

G.2.1 Non-null by Default

H. What's Missing

Bibliography

Index

This document was generated by U-GARYS-VAIO\leavens on July, 13 2011 using texi2html