| Index Entry | Section |
|---|
|
| F | | |
|---|
| F | 4.6 Tokens |
| f | 4.6 Tokens |
| false | 4.6 Tokens |
| false | 4.6 Tokens |
| false | 12.3 Expressions |
| features, level 0 | 2.9.1 Level 0 Features |
| features, level 1 | 2.9.2 Level 1 Features |
| features, level 2 | 2.9.3 Level 2 Features |
| features, level 3 | 2.9.4 Level 3 Features |
| features, level C | 2.9.5 Level C Features |
| features, level X | 2.9.6 Level X Features |
| field | 4.6 Tokens |
| field | 7.1.2 Field and Variable Declarations |
| field | 7.1.2 Field and Variable Declarations |
| field access, and ownership typing rules | 18.6.2 Ownership Typing for Expressions |
| field declarations, in separate files | 17.3 Type Checking Separate Files |
| field initializers | 17.3 Type Checking Separate Files |
| field, defined | 7. Class and Interface Member Declarations |
| field, used | 6.1 Class and Interface Declarations |
| file name for a compilation unit | 5. Compilation Units |
| filename suffixes | 17.1 File Name Suffixes |
| filename suffixes | 17.2 Using Separate Files |
| final | 4.6 Tokens |
| final | 6.2 Modifiers |
| final | 7.1.1.1 Formal Parameters |
| final | 13.1.1 Modifiers for Local Declarations |
| final and model | 6.2.6 Model |
| final, modifier in separate file | 17.3 Type Checking Separate Files |
| final, modifier in separate file | 17.3 Type Checking Separate Files |
| finally | 4.6 Tokens |
| finally | 13. Statements and Annotation Statements |
| Fitzgerald | 1.5 Historical Precedents |
| float | 4.6 Tokens |
| float | 12.3 Expressions |
| float-type-suffix, defined | 4.6 Tokens |
| float-type-suffix, used | 4.6 Tokens |
| floating-point-literal, defined | 4.6 Tokens |
| floating-point-literal, used | 4.6 Tokens |
| for | 4.6 Tokens |
| for | 8.3 Constraints |
| for | 13.2 Loop Statements |
| for-init, defined | 13.2 Loop Statements |
| for-init, used | 13.2 Loop Statements |
| for_example | 4.6 Tokens |
| for_example | 14.2 Redundant Examples |
| forall | 4.6 Tokens |
| forall | 9.6.2 Semantics of non-helper methods |
| forall | 9.6.2 Semantics of non-helper methods |
| forall | 9.9.1.1 Forall Variable Declarations |
| forall-var-declarator, defined | 9.9.1.1 Forall Variable Declarations |
| forall-var-declarator, used | 9.9.1.1 Forall Variable Declarations |
| forall-var-decls, defined | 9.9.1.1 Forall Variable Declarations |
| forall-var-decls, used | 9.9.1 Specification Variable Declarations |
| formal documentation | 1.3 What is JML Good For? |
| formal parameters, and ownership typing rules | 18.6.2 Ownership Typing for Expressions |
| formal specification, reasons for using | 1.3 What is JML Good For? |
| formals, defined | 7.1.1.1 Formal Parameters |
| formals, used | 7.1.1 Method and Constructor Declarations |
| formfeed | 4.1 White Space |
| frame axiom | 1.1 Behavioral Interface Specifications |
| frame axiom | 1.2 A First Example |
| frame axiom | 9.9.9 Assignable Clauses |
| frame axiom, omitted | 9.9.9 Assignable Clauses |
| Freitas, Leo | 1.6 Acknowledgments |
| Fresco | 1.1 Behavioral Interface Specifications |
| fresh predicate | 12.4.9 \fresh |
| fresh, and constructor specifications | 12.4.9 \fresh |
| fresh-expression, defined | 12.4.9 \fresh |
| fresh-expression, used | 12.4 JML Primary Expressions |
| functional abstraction | 8.4 Represents Clauses |
| fundamental concepts | 2. Fundamental Concepts |
|
| G | | |
|---|
| generalized quantifier | 12.4.24.2 Generalized Quantifiers |
| generic-spec-body, defined | Syntax |
| generic-spec-body, used | Syntax |
| generic-spec-case, defined | Syntax |
| generic-spec-case, used | Syntax |
| generic-spec-case, used | Syntax |
| generic-spec-case, used | 9.7 Normal Behavior Specification Cases |
| generic-spec-case, used | 9.8 Exceptional Behavior Specification Cases |
| generic-spec-case-seq, defined | Syntax |
| generic-spec-case-seq, used | Syntax |
| generic-spec-statement-body, defined | 15.6 Specification Statements |
| generic-spec-statement-body, used | 15.6 Specification Statements |
| generic-spec-statement-case, defined | 15.6 Specification Statements |
| generic-spec-statement-case, used | 13.4.3 Refining Statements |
| generic-spec-statement-case, used | 15.6 Specification Statements |
| generic-spec-statement-case-seq, defined | 15.6 Specification Statements |
| generic-spec-statement-case-seq, used | 15.6 Specification Statements |
| ghost | 2.2 Model and Ghost |
| ghost | 2.2 Model and Ghost |
| ghost | 4.6 Tokens |
| ghost | 6.2 Modifiers |
| ghost | 6.2.7 Ghost |
| ghost | 7.1.2.1 JML Modifiers for Fields |
| ghost | 13.1.1 Modifiers for Local Declarations |
| ghost and static, in interfaces | 6.2.7 Ghost |
| ghost features | 2.2 Model and Ghost |
| ghost fields | 2.2 Model and Ghost |
| ghost fields, and namespace | 2.2 Model and Ghost |
| ghost fields, in interfaces | 6.2.7 Ghost |
| ghost vs. model | 6.2.7 Ghost |
| ghost, modifier in separate file | 17.3 Type Checking Separate Files |
| ghost, modifier in separate file | 17.3 Type Checking Separate Files |
| GhostLocals | 13.1.1 Modifiers for Local Declarations |
| goals, of JML | 1. Introduction |
| goals, of JML | 1.3 What is JML Good For? |
| Gosling | 1. Introduction |
| Gosling | 2.4 Privacy Modifiers and Visibility |
| Gosling | 2.7 Expression Evaluation and Undefinedness |
| Gosling | 4.6 Tokens |
| Gosling | 4.6 Tokens |
| Gosling | 5. Compilation Units |
| Gosling | 6.1 Class and Interface Declarations |
| Gosling | 6.1.1 Subtyping for Type Declarations |
| Gosling | 6.2 Modifiers |
| goto | 4.6 Tokens |
| grammar notations | 3. Syntax Notation |
| grammar, conventions for lists | 3. Syntax Notation |
| grammar, start rule | 5. Compilation Units |
| Greene, Robin | 1.6 Acknowledgments |
| grey-box specification | 15.1 Ideas Behind Model Programs |
| Gries | 2.7 Expression Evaluation and Undefinedness |
| group, data | 10. Data Groups |
| group-list, defined | 10.1 Static Data Group Inclusions |
| group-list, defined | 10.2 Dynamic Data Group Mappings |
| group-list, used | 10.1 Static Data Group Inclusions |
| group-list, used | 10.2 Dynamic Data Group Mappings |
| group-name, defined | 10.1 Static Data Group Inclusions |
| group-name, defined | 10.2 Dynamic Data Group Mappings |
| group-name, used | 10.1 Static Data Group Inclusions |
| group-name, used | 10.2 Dynamic Data Group Mappings |
| group-name-prefix, defined | 10.1 Static Data Group Inclusions |
| group-name-prefix, used | 10.1 Static Data Group Inclusions |
| guarded-statement, defined | 15.5 Nondeterministic If Statement |
| guarded-statement, used | 15.5 Nondeterministic If Statement |
| guarded-statements, defined | 15.5 Nondeterministic If Statement |
| guarded-statements, used | 15.5 Nondeterministic If Statement |
| guidelines, for writing assertions | 2.7 Expression Evaluation and Undefinedness |
| Guttag | 1.1 Behavioral Interface Specifications |
| Guttag | 1.2 A First Example |
| Guttag | 1.3 What is JML Good For? |
| Guttag | 1.5 Historical Precedents |
| Guttag | 1.5 Historical Precedents |
| Guttag | 1.5 Historical Precedents |
|