| Index Entry | Section |
|---|
|
| B | | |
|---|
| b | 4.6 Tokens |
| B | 4.6 Tokens |
| B@"{u}chi | 15.1 Ideas Behind Model Programs |
| Back | 1.5 Historical Precedents |
| Back | 15. Model Programs |
| backslash | 4.6 Tokens |
| backspace | 4.6 Tokens |
| Backus | 3. Syntax Notation |
| Baker | 1. Introduction |
| Baker | 1.3 What is JML Good For? |
| Baker | 2.4 Privacy Modifiers and Visibility |
| Baker | 2.4 Privacy Modifiers and Visibility |
| Baker | 2.7 Expression Evaluation and Undefinedness |
| Baker | 7.1.1.3 Pure Methods and Constructors |
| Baker | 14. Redundancy |
| Baker | 14.1 Redundant Implications and Redundantly Clauses |
| Baker | 14.2 Redundant Examples |
| Bandera | 1.4 Status and Plans for JML |
| behavior | 2.3 Lightweight and Heavyweight Specifications |
| behavior | 4.6 Tokens |
| behavior | 9.6 Behavior Specification Cases |
| behavior | Syntax |
| behavior | 9.6.2 Semantics of non-helper methods |
| behavior specification cases, syntax and semantics of | 9.6 Behavior Specification Cases |
| behavior, British spelling of | Syntax |
| behavior, sequential | 1.3 What is JML Good For? |
| behavior-keyword, defined | Syntax |
| behavior-keyword, used | 15.6 Specification Statements |
| behavior-spec-case, defined | Syntax |
| behavior-spec-case, used | 9.5 Heavyweight Specification Cases |
| behavioral interface specification | 1.1 Behavioral Interface Specifications |
| behaviour | 4.6 Tokens |
| behaviour | Syntax |
| benefits, of JML | 1.3 What is JML Good For? |
| big integer type | 19. Safe Math Extensions |
| blank | 4.1 White Space |
| BNF notation | 3. Syntax Notation |
| body of a quantifier | 12.4.24.2 Generalized Quantifiers |
| body, in quantifier | 12.4.24 Quantified Expressions |
| body, of method, in separate files | 17.3 Type Checking Separate Files |
| body, of quantifier | 1.2 A First Example |
| body, of refining statement | 13.4.3 Refining Statements |
| boolean | 4.6 Tokens |
| boolean | 12.3 Expressions |
| boolean-literal, defined | 4.6 Tokens |
| boolean-literal, used | 4.6 Tokens |
| Borgida | 1.1 Behavioral Interface Specifications |
| bound variable, in quantifier | 12.4.24 Quantified Expressions |
| bound variables, modifiers for | 12.4.24.5 Modifiers for Bound Variables |
| bound-var-modifiers, defined | 12.4.24.5 Modifiers for Bound Variables |
| bound-var-modifiers, used | 9.9.1.1 Forall Variable Declarations |
| bound-var-modifiers, used | 9.9.1.2 Old Variable Declarations |
| bound-var-modifiers, used | 12.4.24 Quantified Expressions |
| bound-var-modifiers, used | 12.5 Set Comprehensions |
| Boyland | 9.6.2 Semantics of non-helper methods |
| break | 4.6 Tokens |
| break | 13. Statements and Annotation Statements |
| break, loops containing | 13.2.1 Loop Invariants |
| breaks | 4.6 Tokens |
| breaks | 15.6.2 Breaks Clause |
| breaks-clause, defined | 15.6.2 Breaks Clause |
| breaks-clause, used | 15.6 Specification Statements |
| breaks-keyword, defined | 15.6.2 Breaks Clause |
| breaks-keyword, used | 15.6.2 Breaks Clause |
| breaks_redundantly | 4.6 Tokens |
| breaks_redundantly | 15.6.2 Breaks Clause |
| British, spelling of behavior | Syntax |
| Buechi | 15. Model Programs |
| built-in-type, defined | 12.3 Expressions |
| built-in-type, used | 7.1.2.2 Type-Specs |
| built-in-type, used | 12.3 Expressions |
| Burdy | 1. Introduction |
| Burdy | 1.3 What is JML Good For? |
| Burdy | 1.3 What is JML Good For? |
| Burdy | 1.3 What is JML Good For? |
| byte | 4.6 Tokens |
| byte | 12.3 Expressions |
|
| C | | |
|---|
| C | 4.6 Tokens |
| c | 4.6 Tokens |
| C++-style-comment, defined | 4.3 Comments |
| C++-style-comment, used | 4.3 Comments |
| C-Style comment | 4.3 Comments |
| C-style-body, defined | 4.3 Comments |
| C-style-body, used | 4.3 Comments |
| C-style-comment, defined | 4.3 Comments |
| C-style-comment, used | 4.3 Comments |
| C-style-end, defined | 4.3 Comments |
| C-style-end, used | 4.3 Comments |
| call, post-state of | 9.6.2 Semantics of non-helper methods |
| call, pre-state of | 9.6.2 Semantics of non-helper methods |
| callable | 4.6 Tokens |
| callable | 9.6.2 Semantics of non-helper methods |
| callable | 9.6.2 Semantics of non-helper methods |
| callable | 9.9.11 Callable Clauses |
| callable clause | 9.9.11 Callable Clauses |
| callable clause, omitted | 9.9.11 Callable Clauses |
| callable-clause, defined | 9.9.11 Callable Clauses |
| callable-clause, used | Syntax |
| callable-clause, used | 15.6 Specification Statements |
| callable-keyword, defined | 9.9.11 Callable Clauses |
| callable-keyword, used | 9.9.11 Callable Clauses |
| callable-methods-list, defined | 9.9.11 Callable Clauses |
| callable-methods-list, used | 9.9.11 Callable Clauses |
| callable_redundantly | 4.6 Tokens |
| callable_redundantly | 9.9.11 Callable Clauses |
| captured | 12.4.8 \only_captured |
| captures | 4.6 Tokens |
| captures | 9.6.2 Semantics of non-helper methods |
| captures | 9.6.2 Semantics of non-helper methods |
| captures | 9.9.13 Captures Clauses |
| captures clause | 9.9.13 Captures Clauses |
| captures clause, omitted | 9.9.13 Captures Clauses |
| captures-clause, defined | 9.9.13 Captures Clauses |
| captures-clause, used | Syntax |
| captures-clause, used | 15.6 Specification Statements |
| captures-keyword, defined | 9.9.13 Captures Clauses |
| captures-keyword, used | 9.9.13 Captures Clauses |
| captures_redundantly | 4.6 Tokens |
| captures_redundantly | 9.9.13 Captures Clauses |
| carriage return | 4.1 White Space |
| carriage return | 4.3 Comments |
| carriage return | 4.6 Tokens |
| carriage-return, defined | 4.1 White Space |
| carriage-return, used | 4.1 White Space |
| case | 4.6 Tokens |
| case | 13. Statements and Annotation Statements |
| cast expressions, default ownership modifiers for types in | 18.5 Default Ownership Modifiers |
| casts, and ownership types | 18.7 Casts and Ownership Types |
| catch | 4.6 Tokens |
| catch | 13. Statements and Annotation Statements |
| Chalin | 2.7 Expression Evaluation and Undefinedness |
| Chalin | 2.7 Expression Evaluation and Undefinedness |
| Chalin | 6.2.12 Math Modifiers |
| Chalin | 19. Safe Math Extensions |
| Chalin | 19.1 \bigint |
| Chalin | 19.2 \real |
| changes, incompatible | B. Incompatible Changes |
| char | 4.6 Tokens |
| char | 12.3 Expressions |
| character-literal, defined | 4.6 Tokens |
| character-literal, used | 4.6 Tokens |
| Cheon | 1. Introduction |
| Cheon | 1.1 Behavioral Interface Specifications |
| Cheon | 1.2 A First Example |
| Cheon | 1.3 What is JML Good For? |
| Cheon | 2.2 Model and Ghost |
| choose | 4.6 Tokens |
| choose | 15.4 Nondeterministic Choice Statement |
| choose_if | 4.6 Tokens |
| choose_if | 15.5 Nondeterministic If Statement |
| claim, procedure | 14.1 Redundant Implications and Redundantly Clauses |
| claims, about a specification | 14.1 Redundant Implications and Redundantly Clauses |
| class | 4.6 Tokens |
| class | 6.1 Class and Interface Declarations |
| class | 12.3 Expressions |
| class declaration | 6.1 Class and Interface Declarations |
| class declarations | 6. Type Declarations |
| class initialization predicate | 12.4.21 \is_initialized |
| class invariant, see instance invariant | 8.2.1 Static vs. instance invariants |
| class, inheritance | 6.1.1 Subtyping for Type Declarations |
| class, modifiers for declarations of | 6.1.2 Modifiers for Type Declarations |
| class-block, defined | 6.1 Class and Interface Declarations |
| class-block, used | 6.1 Class and Interface Declarations |
| class-block, used | 12.3 Expressions |
| class-declaration, defined | 6.1 Class and Interface Declarations |
| class-declaration, used | 6. Type Declarations |
| class-declaration, used | 7.1 Java Member Declarations |
| class-extends-clause, defined | 6.1.1 Subtyping for Type Declarations |
| class-extends-clause, used | 6.1 Class and Interface Declarations |
| class-initializer-decl, defined | 7.2 Class Initializer Declarations |
| class-initializer-decl, used | 7. Class and Interface Member Declarations |
| Clifton | 1.4 Status and Plans for JML |
| code | 4.6 Tokens |
| code | Syntax |
| code | 9.7 Normal Behavior Specification Cases |
| code | 9.8 Exceptional Behavior Specification Cases |
| code | 15.3 Details of Model Programs |
| code contract | 16. Specification for Subtypes |
| code contract | 16.2 Code Contracts |
| code, modifier, semantics of | 16.2 Code Contracts |
| code. | 16. Specification for Subtypes |
| code_bigint_math | 4.6 Tokens |
| code_bigint_math | 6.1.2 Modifiers for Type Declarations |
| code_bigint_math | 6.2 Modifiers |
| code_bigint_math | 6.2.12 Math Modifiers |
| code_bigint_math | 6.2.12 Math Modifiers |
| code_java_math | 4.6 Tokens |
| code_java_math | 6.1.2 Modifiers for Type Declarations |
| code_java_math | 6.2 Modifiers |
| code_java_math | 6.2.12 Math Modifiers |
| code_java_math | 6.2.12 Math Modifiers |
| code_safe_math | 4.6 Tokens |
| code_safe_math | 6.1.2 Modifiers for Type Declarations |
| code_safe_math | 6.2 Modifiers |
| code_safe_math | 6.2.12 Math Modifiers |
| code_safe_math | 6.2.12 Math Modifiers |
| Cohen | 12.4.24.2 Generalized Quantifiers |
| Cohen | 12.4.24.3 Numerical Quantifier |
| Cok | G.1 Differences Between JML and Other Tools |
| comment, defined | 4.3 Comments |
| comment, syntax of | 4.3 Comments |
| comment, used | 4. Lexical Conventions |
| comments vs. annotations | 4.4 Annotation Markers |
| comments, annotations in | 1.2 A First Example |
| commit | 9.6.2 Semantics of non-helper methods |
| commit point | 9.6.2 Semantics of non-helper methods |
| compilation unit | 5. Compilation Units |
| compilation unit, and public types | 5. Compilation Units |
| compilation unit, file name for | 5. Compilation Units |
| compilation unit, mutual recursion in | 5. Compilation Units |
| compilation unit, satisfaction of | 5. Compilation Units |
| compilation-unit, defined | 5. Compilation Units |
| completely omitted specification | Semantics |
| completeness, of method specifications | 1.2 A First Example |
| completeness, of specification | 1.2 A First Example |
| compound-statement, defined | 13. Statements and Annotation Statements |
| compound-statement, used | 7.1.1 Method and Constructor Declarations |
| compound-statement, used | 7.2 Class Initializer Declarations |
| compound-statement, used | 13. Statements and Annotation Statements |
| compound-statement, used | 15.3 Details of Model Programs |
| concepts, fundamental | 2. Fundamental Concepts |
| concrete field | 2.2 Model and Ghost |
| concurrency, lack of support in JML | 1.3 What is JML Good For? |
| conditional-expr, defined | 12.3 Expressions |
| conditional-expr, used | 12.3 Expressions |
| const | 4.6 Tokens |
| const | 6.2 Modifiers |
| constant, defined | 12.3 Expressions |
| constant, used | 12.3 Expressions |
| constrained-list, defined | 8.3 Constraints |
| constrained-list, used | 8.3 Constraints |
| constraint | 4.6 Tokens |
| Constraint | 8.3 Constraints |
| constraint | 8.3 Constraints |
| constraint, instance vs. static | 8.3.1 Static vs. instance constraints |
| constraint, static vs. instance | 8.3.1 Static vs. instance constraints |
| constraint-keyword, defined | 8.3 Constraints |
| constraint-keyword, used | 8.3 Constraints |
| constraint_redundantly | 4.6 Tokens |
| constraint_redundantly | 8.3 Constraints |
| constraints, vs. helper | 6.2.9 Helper |
| constructor | 4.6 Tokens |
| constructor | 7.1.1 Method and Constructor Declarations |
| constructor specification | 9. Method Specifications |
| constructor specifications, and \fresh | 12.4.9 \fresh |
| constructor, and invariants | 8.2 Invariants |
| constructor, default, specification of | Semantics |
| constructor, helper | 7.1.1.4 Helper Methods and Constructors |
| constructor, model | 7.1.1.2 Model Methods and Constructors |
| constructor, pure | 7.1.1.3 Pure Methods and Constructors |
| context, ownership | 18.1 Basic Concepts of Universes |
| continue | 4.6 Tokens |
| continue | 13. Statements and Annotation Statements |
| continue | 13.2.2 Loop Variant Functions |
| continues | 4.6 Tokens |
| continues | 15.6.1 Continues Clause |
| continues-clause, defined | 15.6.1 Continues Clause |
| continues-clause, used | 15.6 Specification Statements |
| continues-keyword, defined | 15.6.1 Continues Clause |
| continues-keyword, used | 15.6.1 Continues Clause |
| continues_redundantly | 4.6 Tokens |
| continues_redundantly | 15.6.1 Continues Clause |
| Corbett | 1.4 Status and Plans for JML |
| current ownership context | 18.2 Rep and Peer |
| cycle, virtual machine | 12.4.11 \duration |
|