| Index Entry | Section |
|---|
|
| D | | |
|---|
| D | 4.6 Tokens |
| d | 4.6 Tokens |
| Daikon | 1. Introduction |
| Daikon | 1.3 What is JML Good For? |
| Daikon | E.1 Differences Between JML and Other Tools |
| data group | 10. Data Groups |
| datatype | 1.5 Historical Precedents |
| debug | 12.4.5 Debug Statements |
| debug-statement, defined | 12.4.5 Debug Statements |
| debug-statement, used | 12.4 JML Annotation Statements |
| decimal-integer-literal, defined | 4.6 Tokens |
| decimal-integer-literal, used | 4.6 Tokens |
| decimal-numeral, defined | 4.6 Tokens |
| decimal-numeral, used | 4.6 Tokens |
| decreases | 4.6 Tokens |
| decreases | 12.2.2 Loop Variant Functions |
| decreases_redundantly | 4.6 Tokens |
| decreases_redundantly | 12.2.2 Loop Variant Functions |
| decreasing | 4.6 Tokens |
| decreasing | 12.2.2 Loop Variant Functions |
| decreasing-keyword, defined | 12.2.2 Loop Variant Functions |
| decreasing-keyword, used | 12.2.2 Loop Variant Functions |
| decreasing_redundantly | 4.6 Tokens |
| decreasing_redundantly | 12.2.2 Loop Variant Functions |
| default | 4.6 Tokens |
| default | 12. Statements and Annotation Statements |
| default access | 2.4 Privacy Modifiers and Visibility |
| default constructor, specification of | Semantics |
| default ownership modifiers for types | 18.5 Default Ownership Modifiers |
| default signals clause, and RuntimeExceptions | 9.9.5 Signals-Only Clauses |
| defaults, for lightweight specification cases | Semantics |
| depends, replaced by in and maps | 20.2 Replaced Syntax |
| deprecated syntax | 20. Deprecated and Replaced Syntax |
| description, defined | 4.5 Documentation Comments |
| description, used | 4.5 Documentation Comments |
| design, documentation of | 1.3 What is JML Good For? |
| destructor, and invariants | 8.2 Invariants |
| deterministic, pure method | 7.1.1.3 Pure Methods and Constructors |
| Dhara | 6.1.1 Subtyping for Type Definitions |
| Dhara | 14.1 Ideas Behind Model Programs |
| Dhara | 15.2 Code Contracts |
| Dietl | 4.6 Tokens |
| Dietl | 5. Compilation Units |
| Dietl | 18. Universe Type System |
| Dietl | 18.1 Basic Concepts of Universes |
| Dietl | 18.1 Basic Concepts of Universes |
| Dietl | 18.5 Default Ownership Modifiers |
| Dietl | 18.6.1 Ownership Subtyping |
| Dietl | 18.6.1 Ownership Subtyping |
| digit | 4.6 Tokens |
| digit, defined | 4.6 Tokens |
| digit, defined | 4.6 Tokens |
| digit, used | 4.6 Tokens |
| digit, used | 4.6 Tokens |
| digits, defined | 4.6 Tokens |
| digits, used | 4.6 Tokens |
| dim-exprs, defined | 11.3 Expressions |
| dim-exprs, used | 11.3 Expressions |
| dims, defined | 7.1.2.2 Type-Specs |
| dims, used | 7.1.1 Method and Constructor Declarations |
| dims, used | 7.1.1.1 Formal Parameters |
| dims, used | 7.1.2 Field and Variable Declarations |
| dims, used | 7.1.2.2 Type-Specs |
| dims, used | 8.3 Constraints |
| dims, used | 11.3 Expressions |
| dims, used | 11.4.24 Quantified Expressions |
| dims, used | 17.1 Augmenting Method Declarations |
| dims, used | 17.2 MultiMethods |
| Directory | 14.1 Ideas Behind Model Programs |
| diverges | 4.6 Tokens |
| Diverges | 9.9.7 Diverges Clauses |
| diverges | 9.6.2 Non-helper methods |
| diverges | 9.6.2 Non-helper methods |
| diverges | 9.9.7 Diverges Clauses |
| diverges clause | 9.9.7 Diverges Clauses |
| diverges clause, omitted | 9.9.7 Diverges Clauses |
| diverges-clause, defined | 9.9.7 Diverges Clauses |
| diverges-clause, used | Syntax |
| diverges-clause, used | 14.6 Specification Statements |
| diverges-keyword, defined | 9.9.7 Diverges Clauses |
| diverges-keyword, used | 9.9.7 Diverges Clauses |
| diverges_redundantly | 4.6 Tokens |
| diverges_redundantly | 9.9.7 Diverges Clauses |
| do | 4.6 Tokens |
| do | 12.2 Loop Statements |
| doc-atsign, defined | 4.5 Documentation Comments |
| doc-atsign, used | 4.5 Documentation Comments |
| doc-comment, defined | 4.5 Documentation Comments |
| doc-comment, used | 4. Lexical Conventions |
| doc-comment, used | 4.5 Documentation Comments |
| doc-comment, used | 6.1 Class and Interface Definitions |
| doc-comment, used | 7.1.1 Method and Constructor Declarations |
| doc-comment, used | 7.1.2 Field and Variable Declarations |
| doc-comment-body, defined | 4.5 Documentation Comments |
| doc-comment-body, used | 4.5 Documentation Comments |
| doc-comment-ignored, defined | 4.5 Documentation Comments |
| doc-nl-ws, defined | 4.5 Documentation Comments |
| doc-non-empty-textline, defined | 4.5 Documentation Comments |
| doc-non-empty-textline, used | 4.5 Documentation Comments |
| doc-non-nl-ws , used | 4.5 Documentation Comments |
| doc-non-nl-ws, defined | 4.5 Documentation Comments |
| doc-non-nl-ws, used | 4.5 Documentation Comments |
| documentation comment, lexical grammar within | 4.5 Documentation Comments |
| documentation comments | 4.5 Documentation Comments |
| documentation comments, and annotations | 4.5 Documentation Comments |
| documentation, of design decisions | 1.3 What is JML Good For? |
| ... | 3. Syntax Notation |
| double | 4.6 Tokens |
| double | 11.3 Expressions |
| double quote | 4.6 Tokens |
| duration | 4.6 Tokens |
| duration | 9.6.2 Non-helper methods |
| duration | 9.6.2 Non-helper methods |
| duration | 9.9.15 Duration Clauses |
| duration, specification of | 11.4.11 \duration |
| duration-clause, defined | 9.9.15 Duration Clauses |
| duration-clause, used | Syntax |
| duration-clause, used | 14.6 Specification Statements |
| duration-expression, defined | 11.4.11 \duration |
| duration-expression, used | 11.4 JML Primary Expressions |
| duration-keyword, defined | 9.9.15 Duration Clauses |
| duration-keyword, used | 9.9.15 Duration Clauses |
| duration_redundantly | 4.6 Tokens |
| duration_redundantly | 9.9.15 Duration Clauses |
| dynamic type of an expression | 11.4.16 \typeof |
|