| Index Entry | Section |
|---|
|
| H | | |
|---|
| Hall | 1.3 What is JML Good For? |
| handbook, for LSL | 1.5 Historical Precedents |
| Handbook, for LSL | 1.5 Historical Precedents |
| handler, defined | 13. Statements and Annotation Statements |
| has | 12.5 Set Comprehensions |
| Hayes | 1.1 Behavioral Interface Specifications |
| Hayes | 1.5 Historical Precedents |
| Heavyweight | Semantics |
| heavyweight example | 14.2 Redundant Examples |
| heavyweight specification | 1.2 A First Example |
| heavyweight specification | 2.3 Lightweight and Heavyweight Specifications |
| heavyweight specification case | 9.5 Heavyweight Specification Cases |
| heavyweight specification, vs. lightweight | 1.2 A First Example |
| heavyweight-spec-case, defined | 9.5 Heavyweight Specification Cases |
| heavyweight-spec-case, used | 9.2 Organization of Method Specifications |
| helper | 4.6 Tokens |
| helper | 6.2 Modifiers |
| helper | 6.2.9 Helper |
| helper | 7.1.1.4 Helper Methods and Constructors |
| helper | 8.2 Invariants |
| helper | 8.2 Invariants |
| helper constructor, and invariants | 8.2 Invariants |
| helper method, and invariants | 8.2 Invariants |
| helper, and invariants | 6.2.9 Helper |
| helper, and private | 6.2.9 Helper |
| hence-by-keyword, defined | 13.4.6 Hence By Statements |
| hence-by-keyword, used | 13.4.6 Hence By Statements |
| hence-by-statement, defined | 13.4.6 Hence By Statements |
| hence-by-statement, used | 13.4 JML Annotation Statements |
| hence_by | 4.6 Tokens |
| hence_by | 13.4.6 Hence By Statements |
| hence_by_redundantly | 4.6 Tokens |
| hence_by_redundantly | 13.4.6 Hence By Statements |
| hex-digit, defined | 4.6 Tokens |
| hex-digit, used | 4.6 Tokens |
| hex-integer-literal, defined | 4.6 Tokens |
| hex-integer-literal, used | 4.6 Tokens |
| hex-numeral, defined | 4.6 Tokens |
| hex-numeral, used | 4.6 Tokens |
| higher-order method specification | 15.1 Ideas Behind Model Programs |
| history constraint | 6.1.1 Subtyping for Type Declarations |
| history constraint | 11. Specification Inheritance |
| history constraints, vs. helper | 6.2.9 Helper |
| history-constraint, defined | 8.3 Constraints |
| history-constraint, used | 8. Type Specifications |
| Hoare | 1.5 Historical Precedents |
| Hoare | 1.5 Historical Precedents |
| Hoare | 2.2 Model and Ghost |
| Holmes | 1. Introduction |
| Horning | 1.1 Behavioral Interface Specifications |
| Horning | 1.3 What is JML Good For? |
| Horning | 1.5 Historical Precedents |
| Horning | 1.5 Historical Precedents |
| Huisman | 1.3 What is JML Good For? |
| Huisman | 1.3 What is JML Good For? |
| Hussain, Faraz | 1.6 Acknowledgments |
|
| I | | |
|---|
| ident, defined | 4.6 Tokens |
| ident, used | 4. Lexical Conventions |
| ident, used | 5.1 Package Declarations |
| ident, used | 5.2 Import Declarations |
| ident, used | 6.1 Class and Interface Declarations |
| ident, used | 6.2.2 Java Annotations |
| ident, used | 7.1.1 Method and Constructor Declarations |
| ident, used | 7.1.1.1 Formal Parameters |
| ident, used | 7.1.2 Field and Variable Declarations |
| ident, used | 8.3 Constraints |
| ident, used | 8.7 Readable If Clauses |
| ident, used | 8.8 Writable If Clauses |
| ident, used | 8.9 Monitors For Clause |
| ident, used | 9.9.4 Signals Clauses |
| ident, used | 10.1 Static Data Group Inclusions |
| ident, used | 10.2 Dynamic Data Group Mappings |
| ident, used | 12.3 Expressions |
| ident, used | 12.4.2 \old and \pre |
| ident, used | 12.4.23 \lblneg and \lblpos |
| ident, used | 12.4.24 Quantified Expressions |
| ident, used | 12.5 Set Comprehensions |
| ident, used | 12.7 Store Refs |
| ident, used | 13. Statements and Annotation Statements |
| ident, used | 13.2 Loop Statements |
| ident, used | 13.2 Loop Statements |
| ident, used | 15.6.1 Continues Clause |
| identifiers | 4.6 Tokens |
| if | 4.6 Tokens |
| if | 8.7 Readable If Clauses |
| if | 8.8 Writable If Clauses |
| if | 9.9.12 Measured By Clauses |
| if | 9.9.14 Working Space Clauses |
| if | 9.9.15 Duration Clauses |
| if | 13. Statements and Annotation Statements |
| ignored-at-in-annotation, defined | 4.4 Annotation Markers |
| ignored-at-in-annotation, used | 4.4 Annotation Markers |
| immutable | 6.1.2.1 Pure Type Declarations |
| immutable, vs. pure | 6.1.2.1 Pure Type Declarations |
| implementation of interfaces | 6.1.1 Subtyping for Type Declarations |
| implements | 4.6 Tokens |
| implements | 6.1.1 Subtyping for Type Declarations |
| implements, for classes | 6.1.1 Subtyping for Type Declarations |
| implements-clause, defined | 6.1.1 Subtyping for Type Declarations |
| implements-clause, used | 6.1 Class and Interface Declarations |
| implements-clause, used | 6.1.1 Subtyping for Type Declarations |
| implication, redundant | 14.1 Redundant Implications and Redundantly Clauses |
| implication, see ==> | 12.6.3 Forward and Reverse Implication Operators |
| implications, defined | 14.1 Redundant Implications and Redundantly Clauses |
| implications, used | 14. Redundancy |
| implicitly nullable | 6.2.13 Nullity Modifiers |
| ImplicitOld | 9.9.6 Parameters in Postconditions |
| implies-expr, defined | 12.3 Expressions |
| implies-expr, used | 12.3 Expressions |
| implies-non-backward-expr, defined | 12.3 Expressions |
| implies-non-backward-expr, used | 12.3 Expressions |
| implies_that | 4.6 Tokens |
| implies_that | 14.1 Redundant Implications and Redundantly Clauses |
| import | 4.6 Tokens |
| import | 5.2 Import Declarations |
| import declaration | 5.2 Import Declarations |
| import, model | 5.2 Import Declarations |
| import-declaration, defined | 5.2 Import Declarations |
| import-declaration, used | 5. Compilation Units |
| in | 4.6 Tokens |
| in | 10.1 Static Data Group Inclusions |
| in-group-clause, defined | 10.1 Static Data Group Inclusions |
| in-group-clause, used | 10. Data Groups |
| in-keyword, defined | 10.1 Static Data Group Inclusions |
| in-keyword, used | 10.1 Static Data Group Inclusions |
| in_redundantly | 4.6 Tokens |
| in_redundantly | 10.1 Static Data Group Inclusions |
| inclusive-or-expr, defined | 12.3 Expressions |
| inclusive-or-expr, used | 12.3 Expressions |
| incompatible changes | B. Incompatible Changes |
| InconsistentMethodSpec | 9.8.1 Pragmatics of Exceptional Behavior Specifications Cases |
| InconsistentMethodSpec2 | 9.8.1 Pragmatics of Exceptional Behavior Specifications Cases |
| infinite precision numeric types | 19. Safe Math Extensions |
| influences, on JML evolution | 1.4 Status and Plans for JML |
| informal descriptions | 4.6 Tokens |
| informal-description, defined | 4.6 Tokens |
| informal-description, used | 4. Lexical Conventions |
| informal-description, used | 12.4 JML Primary Expressions |
| informal-description, used | 12.7 Store Refs |
| information hiding, in assignable clauses | 10. Data Groups |
| inheritance | 6.1.1 Subtyping for Type Declarations |
| inheritance | 6.1.1 Subtyping for Type Declarations |
| inheritance, multiple | 6.1.1 Subtyping for Type Declarations |
| inheritance, of JML features | 6.1.1 Subtyping for Type Declarations |
| inheritance, of JML features | 6.1.1 Subtyping for Type Declarations |
| inheritance, of JML features | 11. Specification Inheritance |
| inheritance, of model methods from interfaces | 6.1.1 Subtyping for Type Declarations |
| inheritance, of specifications | 6.1.1 Subtyping for Type Declarations |
| inheritance, of specifications | 6.1.1 Subtyping for Type Declarations |
| inheritance, of specifications | 11. Specification Inheritance |
| inherits | 6.1.1 Subtyping for Type Declarations |
| initialization, specification that a class is | 12.4.21 \is_initialized |
| initializer | 4.6 Tokens |
| initializer, defined | 7.1.2 Field and Variable Declarations |
| initializer, defined | 12.3 Expressions |
| initializer, separate files | 17.3 Type Checking Separate Files |
| initializer, used | 7.1.2 Field and Variable Declarations |
| initializer, used | 7.2 Class Initializer Declarations |
| initializer, used | 12.3 Expressions |
| initializer-list, defined | 7.1.2 Field and Variable Declarations |
| initializer-list, used | 7.1.2 Field and Variable Declarations |
| initializers, for fields field | 17.3 Type Checking Separate Files |
| initializers, separate files | 17.3 Type Checking Separate Files |
| initially | 4.6 Tokens |
| initially | 8.5 Initially Clauses |
| initially, clause and separate files | 17.3 Type Checking Separate Files |
| initially-clause, defined | 8.5 Initially Clauses |
| initially-clause, used | 8. Type Specifications |
| instance | 2.5 Instance vs. Static |
| instance | 4.6 Tokens |
| instance | 6.2 Modifiers |
| instance | 6.2.8 Instance |
| instance | 7.1.2.1 JML Modifiers for Fields |
| instance | 8.2.1 Static vs. instance invariants |
| instance | 8.3.1 Static vs. instance constraints |
| instance constraint | 8.3.1 Static vs. instance constraints |
| instance features | 2.5 Instance vs. Static |
| instance invariant | 8.2 Invariants |
| instance invariant | 8.2.1 Static vs. instance invariants |
| instance invariant | 8.2.1 Static vs. instance invariants |
| instance vs. final, in interfaces | 7.1.2.1 JML Modifiers for Fields |
| instance vs. static | 7.1.2.1 JML Modifiers for Fields |
| instanceof | 4.6 Tokens |
| instanceof | 12.3 Expressions |
| instanceof, and ownership types | 18.7 Casts and Ownership Types |
| instanceof, default ownership modifiers for | 18.5 Default Ownership Modifiers |
| instanceof, default ownership modifiers for types in | 18.5 Default Ownership Modifiers |
| int | 4.6 Tokens |
| int | 12.3 Expressions |
| integer-literal, defined | 4.6 Tokens |
| integer-literal, used | 4.6 Tokens |
| integer-type-suffix, defined | 4.6 Tokens |
| integer-type-suffix, used | 4.6 Tokens |
| interface | 4.6 Tokens |
| interface | 6.1 Class and Interface Declarations |
| interface declaration | 6.1 Class and Interface Declarations |
| interface declarations | 6. Type Declarations |
| interface specification | 1.1 Behavioral Interface Specifications |
| interface, field | 1.1 Behavioral Interface Specifications |
| interface, method | 1.1 Behavioral Interface Specifications |
| interface, modifiers for declarations of | 6.1.2 Modifiers for Type Declarations |
| interface, type | 1.1 Behavioral Interface Specifications |
| interface-declaration, defined | 6.1 Class and Interface Declarations |
| interface-declaration, defined | 6.1.1 Subtyping for Type Declarations |
| interface-declaration, used | 6. Type Declarations |
| interface-declaration, used | 7.1 Java Member Declarations |
| interface-extends, defined | 6.1.1 Subtyping for Type Declarations |
| interface-extends, used | 6.1 Class and Interface Declarations |
| interfaces, and default modifier for fields | 6.2.6 Model |
| interfaces, and default modifier for fields | 6.2.7 Ghost |
| interfaces, and ghost fields | 6.2.7 Ghost |
| interfaces, and model fields | 6.2.6 Model |
| IntHeap | 1.2 A First Example |
| Invariant | 8.2 Invariants |
| invariant | 4.6 Tokens |
| invariant | 8.2 Invariants |
| invariant, and helper constructors | 7.1.1.4 Helper Methods and Constructors |
| invariant, and helper methods | 7.1.1.4 Helper Methods and Constructors |
| invariant, assuming | 8.2 Invariants |
| invariant, defined | 8.2 Invariants |
| invariant, enforcement | 8.2 Invariants |
| invariant, establishing | 8.2 Invariants |
| invariant, for an object | 12.4.22 \invariant_for |
| invariant, instance | 8.2 Invariants |
| invariant, instance vs. static | 8.2.1 Static vs. instance invariants |
| invariant, preserving | 8.2 Invariants |
| invariant, reasoning about | 8.2 Invariants |
| invariant, static | 8.2 Invariants |
| invariant, static vs. instance | 8.2.1 Static vs. instance invariants |
| invariant, used | 8. Type Specifications |
| invariant, used | 15.3 Details of Model Programs |
| invariant-for-expression, defined | 12.4.22 \invariant_for |
| invariant-for-expression, used | 12.4 JML Primary Expressions |
| invariant-keyword, defined | 8.2 Invariants |
| invariant-keyword, used | 8.2 Invariants |
| invariant_redundantly | 4.6 Tokens |
| invariant_redundantly | 8.2 Invariants |
| invariants, and modularity | 8.2 Invariants |
| invariants, vs. helper | 6.2.9 Helper |
| is-initialized-expression, defined | 12.4.21 \is_initialized |
| is-initialized-expression, used | 12.4 JML Primary Expressions |
| isAssignableFrom, method of java.lang.Class | 12.6.1 Subtype operator |
| ISO | 1.5 Historical Precedents |
|