| Index Entry | Section |
|---|
|
| J | | |
|---|
| Jackson | 16.2 Code Contracts |
| Jacobs | 1.3 What is JML Good For? |
| Jacobs | 1.3 What is JML Good For? |
| Jacobs | 1.6 Acknowledgments |
| Java | 1. Introduction |
| Java annotation | 6.2.2 Java Annotations |
| `java' filename suffix | 17.1 File Name Suffixes |
| Java modifiers | 6.2 Modifiers |
| Java reserved words | 4.6 Tokens |
| Java virtual machine error, and method semantics | 9.6.2 Semantics of non-helper methods |
| Java vs. JML-only names, resolving conflicts | 2.2 Model and Ghost |
| java-annotation, defined | 6.2.2 Java Annotations |
| java-annotation, used | 6.2 Modifiers |
| java-annotation, used | 6.2.2 Java Annotations |
| java-annotations, defined | 6.2.2 Java Annotations |
| java-annotations, used | 5.1 Package Declarations |
| java-literal, defined | 4.6 Tokens |
| java-literal, used | 4. Lexical Conventions |
| java-literal, used | 12.3 Expressions |
| java-operator, defined | 4.6 Tokens |
| java-operator, used | 4.6 Tokens |
| java-reserved-word, defined | 4.6 Tokens |
| java-reserved-word, used | 4.6 Tokens |
| java-separator, defined | 4.6 Tokens |
| java-separator, used | 4.6 Tokens |
| java-special-symbol, defined | 4.6 Tokens |
| java-special-symbol, used | 4.6 Tokens |
| java-universe-reserved, defined | 4.6 Tokens |
| java.lang.Class, and \TYPE | 7.1.2.2 Type-Specs |
| java.lang.Class, vs. \type() | 12.4.18 \type |
| javadoc | 4.5 Documentation Comments |
| JML annotation | 4.4 Annotation Markers |
| `jml' filename suffix | 17.1 File Name Suffixes |
| JML keywords, where recognized | 4.6 Tokens |
| JML status and plans | 1.4 Status and Plans for JML |
| JML web site | 1. Introduction |
| JML, evolution | 1.4 Status and Plans for JML |
| JML, plans | 1.4 Status and Plans for JML |
| JML, status | 1.4 Status and Plans for JML |
| jml-annotation-statement, defined | 13.4 JML Annotation Statements |
| jml-annotation-statement, used | 13. Statements and Annotation Statements |
| jml-annotation-statement, used | 13. Statements and Annotation Statements |
| jml-compound-statement, defined | 15.3 Details of Model Programs |
| jml-compound-statement, used | 15.3 Details of Model Programs |
| jml-compound-statement, used | 15.4 Nondeterministic Choice Statement |
| jml-compound-statement, used | 15.5 Nondeterministic If Statement |
| jml-data-group-clause, defined | 10. Data Groups |
| jml-data-group-clause, used | 7.1.2 Field and Variable Declarations |
| jml-data-group-clause, used | 7.1.2 Field and Variable Declarations |
| jml-declaration, defined | 8. Type Specifications |
| jml-declaration, used | 7. Class and Interface Member Declarations |
| jml-keyword, defined | 4.6 Tokens |
| jml-keyword, used | 4.6 Tokens |
| jml-modifier, defined | 6.2 Modifiers |
| jml-modifier, used | 6.2 Modifiers |
| JML-only vs. Java names, resolving conflicts | 2.2 Model and Ghost |
| jml-predicate-keyword, defined | 4.6 Tokens |
| jml-predicate-keyword, used | 4.6 Tokens |
| jml-primary, defined | 12.4 JML Primary Expressions |
| jml-primary, used | 12.3 Expressions |
| jml-special-symbol, defined | 4.6 Tokens |
| jml-special-symbol, used | 4.6 Tokens |
| jml-specs, defined | 4.5 Documentation Comments |
| jml-specs, used | 4.5 Documentation Comments |
| jml-statement, defined | 15.3 Details of Model Programs |
| jml-statement, used | 15.5 Nondeterministic If Statement |
| jml-tag, defined | 4.5 Documentation Comments |
| jml-tag, used | 4.5 Documentation Comments |
| jml-universe-keyword, defined | 4.6 Tokens |
| jml-universe-keyword, used | 4.6 Tokens |
| jml-universe-pkeyword, defined | 4.6 Tokens |
| jml-universe-pkeyword, used | 4.6 Tokens |
| jmlc | 1.3 What is JML Good For? |
| jmlc | 12.4.24.4 Executability of Quantified Expressions |
| jmlc, warnings for non-executable assertions | 12.4.24.4 Executability of Quantified Expressions |
| jmldoc | 1.3 What is JML Good For? |
| Jones | 1.5 Historical Precedents |
| Joy | 4.6 Tokens |
| Joy | 4.6 Tokens |
|
| K | | |
|---|
| key, negative | 4.4 Annotation Markers |
| key, positive | 4.4 Annotation Markers |
| keys, for conditional annotation, syntax | 4.4 Annotation Markers |
| keyword, defined | 4.6 Tokens |
| keyword, used | 4. Lexical Conventions |
| keywords | 4.6 Tokens |
| Khurshid | 16.2 Code Contracts |
| Kiczales | 16. Specification for Subtypes |
| Kiniry | G.1 Differences Between JML and Other Tools |
|
| L | | |
|---|
| L | 4.6 Tokens |
| l | 4.6 Tokens |
| label expression (negative) | 12.4.23 \lblneg and \lblpos |
| label expression (positive) | 12.4.23 \lblneg and \lblpos |
| Lamping | 16. Specification for Subtypes |
| Lamport | 1.1 Behavioral Interface Specifications |
| language level 0 features | 2.9.1 Level 0 Features |
| language level 1 features | 2.9.2 Level 1 Features |
| language level 2 features | 2.9.3 Level 2 Features |
| language level 3 features | 2.9.4 Level 3 Features |
| language level C features | 2.9.5 Level C Features |
| language level X features | 2.9.6 Level X Features |
| language levels | 2.9 Language Levels |
| language levels, and learning JML | 2.9 Language Levels |
| language levels, and tools | 2.9 Language Levels |
| Larch | 1.1 Behavioral Interface Specifications |
| Larch | 1.5 Historical Precedents |
| Larch Shared Language (LSL) | 1.1 Behavioral Interface Specifications |
| Larch style specification language | 1.1 Behavioral Interface Specifications |
| Larch/C++ | 1.5 Historical Precedents |
| Larsen | 1.5 Historical Precedents |
| lblneg-expression, defined | 12.4.23 \lblneg and \lblpos |
| lblneg-expression, used | 12.4 JML Primary Expressions |
| lblpos-expression, defined | 12.4.23 \lblneg and \lblpos |
| lblpos-expression, used | 12.4 JML Primary Expressions |
| learning JML, and language levels | 2.9 Language Levels |
| Leavens | 1. Introduction |
| Leavens | 1.1 Behavioral Interface Specifications |
| Leavens | 1.2 A First Example |
| Leavens | 1.3 What is JML Good For? |
| Leavens | 1.3 What is JML Good For? |
| Leavens | 1.3 What is JML Good For? |
| Leavens | 1.5 Historical Precedents |
| Leavens | 2.4 Privacy Modifiers and Visibility |
| Leavens | 2.4 Privacy Modifiers and Visibility |
| Leavens | 2.7 Expression Evaluation and Undefinedness |
| Leavens | 2.7 Expression Evaluation and Undefinedness |
| Leavens | 6.1.1 Subtyping for Type Declarations |
| Leavens | 6.2.9 Helper |
| Leavens | 7.1.1.3 Pure Methods and Constructors |
| Leavens | 8.2 Invariants |
| Leavens | 11. Specification Inheritance |
| Leavens | 11. Specification Inheritance |
| Leavens | 14. Redundancy |
| Leavens | 14.1 Redundant Implications and Redundantly Clauses |
| Leavens | 14.2 Redundant Examples |
| Leavens | 15.1 Ideas Behind Model Programs |
| Leavens | 15.1 Ideas Behind Model Programs |
| Leavens | 16. Specification for Subtypes |
| Leavens | 16. Specification for Subtypes |
| Leavens | 16.2 Code Contracts |
| Leavens | 18.1 Basic Concepts of Universes |
| Ledgard | 3. Syntax Notation |
| Leino | 1.1 Behavioral Interface Specifications |
| Leino | 1.3 What is JML Good For? |
| Leino | 1.6 Acknowledgments |
| Leino | 2.2 Model and Ghost |
| Leino | 2.4 Privacy Modifiers and Visibility |
| Leino | 4.4 Annotation Markers |
| Leino | 6.2.10 Monitored |
| Leino | 6.2.11 Uninitialized |
| Leino | 7.1.2.1 JML Modifiers for Fields |
| Leino | 12.4.19 \lockset |
| Leino | G.1 Differences Between JML and Other Tools |
| letter, defined | 4.6 Tokens |
| letter, used | 4.2 Lexical Pragmas |
| letter, used | 4.5 Documentation Comments |
| letter, used | 4.6 Tokens |
| letter-or-digit, defined | 4.6 Tokens |
| letter-or-digit, used | 4.6 Tokens |
| level 0, JML features | 2.9 Language Levels |
| level 0, JML features | 2.9.1 Level 0 Features |
| level 1, JML features | 2.9 Language Levels |
| level 1, JML features | 2.9.2 Level 1 Features |
| level 2, JML features | 2.9 Language Levels |
| level 2, JML features | 2.9.3 Level 2 Features |
| level 3, JML features | 2.9 Language Levels |
| level 3, JML features | 2.9.4 Level 3 Features |
| level C, JML features | 2.9 Language Levels |
| level C, JML features | 2.9.5 Level C Features |
| level X, JML features | 2.9 Language Levels |
| level X, JML features | 2.9.6 Level X Features |
| levels, of language support | 2.9 Language Levels |
| lexeme, defined | 4. Lexical Conventions |
| lexeme, used | 4. Lexical Conventions |
| lexical conventions | 4. Lexical Conventions |
| lexical-pragma, defined | 4.2 Lexical Pragmas |
| lexical-pragma, used | 4. Lexical Conventions |
| Lightweight | Semantics |
| lightweight example | 14.2 Redundant Examples |
| lightweight specification | 2.3 Lightweight and Heavyweight Specifications |
| lightweight specification case | 9.4 Lightweight Specification Cases |
| lightweight specification, example of | 1.2 A First Example |
| lightweight specification, vs. heavyweight | 1.2 A First Example |
| lightweight specifications and access control | 2.4 Privacy Modifiers and Visibility |
| lightweight-spec-case, defined | Syntax |
| lightweight-spec-case, used | 9.2 Organization of Method Specifications |
| Liskov | 1.2 A First Example |
| Liskov | 1.5 Historical Precedents |
| list vs. sequence, in grammar | 3. Syntax Notation |
| literals | 4.6 Tokens |
| local-declaration, defined | 13.1 Local Declaration Statements |
| local-declaration, used | 13. Statements and Annotation Statements |
| local-declaration, used | 13.2 Loop Statements |
| local-modifier, defined | 13.1.1 Modifiers for Local Declarations |
| local-modifier, used | 13.1.1 Modifiers for Local Declarations |
| local-modifiers, defined | 13.1.1 Modifiers for Local Declarations |
| local-modifiers, used | 13.1 Local Declaration Statements |
| location | 1.2 A First Example |
| location | 2.6 Locations and Aliasing |
| location | 10. Data Groups |
| locking order | 12.6.4 Lockset Ordering |
| locks held by a thread | 12.4.19 \lockset |
| lockset-expression, defined | 12.4.19 \lockset |
| lockset-expression, used | 12.4 JML Primary Expressions |
| logic, three-valued | 2.7 Expression Evaluation and Undefinedness |
| logic, two-valued | 2.7 Expression Evaluation and Undefinedness |
| logical implication, see ==> | 12.6.3 Forward and Reverse Implication Operators |
| logical rules, valid in JML | 2.7 Expression Evaluation and Undefinedness |
| logical-and-expr, defined | 12.3 Expressions |
| logical-and-expr, used | 12.3 Expressions |
| logical-or-expr, defined | 12.3 Expressions |
| logical-or-expr, used | 12.3 Expressions |
| long | 4.6 Tokens |
| long | 12.3 Expressions |
| LOOP | 1.3 What is JML Good For? |
| loop, exiting via break | 13.2.1 Loop Invariants |
| loop-invariant, defined | 13.2.1 Loop Invariants |
| loop-invariant, used | 13.2 Loop Statements |
| loop-stmt, defined | 13.2 Loop Statements |
| loop_invariant | 4.6 Tokens |
| loop_invariant | 13.2.1 Loop Invariants |
| loop_invariant_redundantly | 4.6 Tokens |
| loop_invariant_redundantly | 13.2.1 Loop Invariants |
| LSL | 1.1 Behavioral Interface Specifications |
| LSL Handbook | 1.5 Historical Precedents |
|