| Index Entry | Section |
|---|
|
| T | | |
|---|
| tab | 4.1 White Space |
| tab | 4.6 Tokens |
| table of precedence | 12.3 Expressions |
| tagged-paragraph, defined | 4.5 Documentation Comments |
| tagged-paragraph, used | 4.5 Documentation Comments |
| Tan | 14.1 Redundant Implications and Redundantly Clauses |
| target-label, used | 15.6.1 Continues Clause |
| target-label, used | 15.6.2 Breaks Clause |
| terminal symbols, notation | 3. Syntax Notation |
| termination, of pure methods | 7.1.1.3 Pure Methods and Constructors |
| terminology, for invariants | 8.2.1 Static vs. instance invariants |
| this | 4.6 Tokens |
| this | 8.2.1 Static vs. instance invariants |
| this | 8.3 Constraints |
| this | 8.3 Constraints |
| this | 8.3.1 Static vs. instance constraints |
| this | 10.1 Static Data Group Inclusions |
| this | 12.3 Expressions |
| this | 12.3 Expressions |
| this | 12.7 Store Refs |
| this | 18.2 Rep and Peer |
| this, and rep | 18.2 Rep and Peer |
| thread, specifying locks held by | 12.4.19 \lockset |
| threads, specification of | 1.3 What is JML Good For? |
| throw | 4.6 Tokens |
| throw | 13. Statements and Annotation Statements |
| throw | 13. Statements and Annotation Statements |
| throws | 4.6 Tokens |
| throws | 7.1.1 Method and Constructor Declarations |
| throws-clause, defined | 7.1.1 Method and Constructor Declarations |
| throws-clause, used | 7.1.1 Method and Constructor Declarations |
| time, specification of | 12.4.11 \duration |
| time, virtual machine cycle | 12.4.11 \duration |
| token, defined | 4. Lexical Conventions |
| token, used | 4. Lexical Conventions |
| tokens | 4.6 Tokens |
| tool support | 1.3 What is JML Good For? |
| tool support | 1.3 What is JML Good For? |
| tools and annotations | 4.4 Annotation Markers |
| tools, advice for builders of | 2.9 Language Levels |
| top-level-declaration, defined | 5. Compilation Units |
| top-level-declaration, used | 5. Compilation Units |
| total correctness | 9.9.7 Diverges Clauses |
| trait | 1.5 Historical Precedents |
| trait function | 1.5 Historical Precedents |
| transient | 4.6 Tokens |
| transient | 6.2 Modifiers |
| true | 4.6 Tokens |
| true | 4.6 Tokens |
| true | 12.3 Expressions |
| try | 4.6 Tokens |
| try | 13. Statements and Annotation Statements |
| try-block, defined | 13. Statements and Annotation Statements |
| try-block, used | 13. Statements and Annotation Statements |
| two-valued logic | 2.7 Expression Evaluation and Undefinedness |
| type | 2.1 Types can be Classes and Interfaces |
| type checking | 1.3 What is JML Good For? |
| type checking, with ownership types | 18.6.2 Ownership Typing for Expressions |
| type declarations | 6. Type Declarations |
| type specs, for declarations | 7.1.2.2 Type-Specs |
| type system, Universe | 18. Universe Type System |
| type, abstract | 1.5 Historical Precedents |
| type, defined | 7.1.2.2 Type-Specs |
| type, modifiers for declarations of | 6.1.2 Modifiers for Type Declarations |
| type, specifying in a declaration | 7.1.2.2 Type-Specs |
| type, used | 7.1.2.2 Type-Specs |
| type, used | 12.3 Expressions |
| type, used | 12.4.18 \type |
| type-declaration, defined | 6. Type Declarations |
| type-declaration, used | 5. Compilation Units |
| type-expression, defined | 12.4.18 \type |
| type-expression, used | 12.4 JML Primary Expressions |
| type-spec, defined | 7.1.2.2 Type-Specs |
| type-spec, used | 7.1.1 Method and Constructor Declarations |
| type-spec, used | 7.1.1.1 Formal Parameters |
| type-spec, used | 7.1.2 Field and Variable Declarations |
| type-spec, used | 8.3 Constraints |
| type-spec, used | 9.9.1.1 Forall Variable Declarations |
| type-spec, used | 9.9.1.2 Old Variable Declarations |
| type-spec, used | 12.3 Expressions |
| type-spec, used | 12.4.24 Quantified Expressions |
| type-spec, used | 12.5 Set Comprehensions |
| type-spec, used | 13.2 Loop Statements |
| typeof expression | 12.4.16 \typeof |
| typeof-expression, defined | 12.4.16 \typeof |
| typeof-expression, used | 12.4 JML Primary Expressions |
| types, comparing | 12.6.1 Subtype operator |
| types, marking in expressions | 12.4.18 \type |
|
| U | | |
|---|
| unary-expr, defined | 12.3 Expressions |
| unary-expr, used | 12.3 Expressions |
| unary-expr-not-plus-minus, defined | 12.3 Expressions |
| unary-expr-not-plus-minus, used | 12.3 Expressions |
| undefinedness, in expression evaluation | 2.7 Expression Evaluation and Undefinedness |
| underspecified total functions | 2.7 Expression Evaluation and Undefinedness |
| unicode-escape, defined | 4.6 Tokens |
| unicode-escape, used | 4.6 Tokens |
| uninitialized | 4.6 Tokens |
| uninitialized | 6.2 Modifiers |
| uninitialized | 6.2.11 Uninitialized |
| Universe | 5. Compilation Units |
| Universe keywords, where recognized | 4.6 Tokens |
| universe type system | 18. Universe Type System |
| Universe type system | 18. Universe Type System |
| Universe type system syntax | 4.6 Tokens |
| Universe type system, basic concepts | 18.1 Basic Concepts of Universes |
| universe type system, options for | 18. Universe Type System |
| unreachable | 4.6 Tokens |
| unreachable | 13.4.4 Unreachable Statements |
| unreachable-statement, defined | 13.4.4 Unreachable Statements |
| unreachable-statement, used | 13.4 JML Annotation Statements |
| usefulness, of JML | 1.3 What is JML Good For? |
| uses, of JML | 1.3 What is JML Good For? |
| utility, of JML | 1.3 What is JML Good For? |
|