JML Reference Manual: Table of Contents (original) (raw)

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.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
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.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
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-leavens-nd\leavens on _May, 31 2013_using texi2html