| Index Entry | Section |
|---|
|
| M | | |
|---|
| Müeller | 2.4 Privacy Modifiers and Visibility |
| Müeller | 8.2 Invariants |
| Müeller | 18.1 Basic Concepts of Universes |
| Müller | 1.6 Acknowledgments |
| Müller | 4.6 Tokens |
| Müller | 5. Compilation Units |
| Müller | 6.2.9 Helper |
| Müller | 18. Universe Type System |
| Müller | 18.1 Basic Concepts of Universes |
| Müller | 18.1 Basic Concepts of Universes |
| Müller | 18.5 Default Ownership Modifiers |
| Müller | 18.6.1 Ownership Subtyping |
| Müller | 18.6.1 Ownership Subtyping |
| maintaining | 4.6 Tokens |
| maintaining | 13.2.1 Loop Invariants |
| maintaining-keyword, defined | 13.2.1 Loop Invariants |
| maintaining-keyword, used | 13.2.1 Loop Invariants |
| maintaining_redundantly | 4.6 Tokens |
| maintaining_redundantly | 13.2.1 Loop Invariants |
| maps | 4.6 Tokens |
| maps | 10.2 Dynamic Data Group Mappings |
| maps-array-ref-expr, defined | 10.2 Dynamic Data Group Mappings |
| maps-array-ref-expr, used | 10.2 Dynamic Data Group Mappings |
| maps-into-clause, defined | 10.2 Dynamic Data Group Mappings |
| maps-into-clause, used | 10. Data Groups |
| maps-into-clause, used | 10.2 Dynamic Data Group Mappings |
| maps-keyword, defined | 10.2 Dynamic Data Group Mappings |
| maps-keyword, used | 10.2 Dynamic Data Group Mappings |
| maps-member-ref-expr, defined | 10.2 Dynamic Data Group Mappings |
| maps-member-ref-expr, used | 10.2 Dynamic Data Group Mappings |
| maps-spec-array-dim, defined | 10.2 Dynamic Data Group Mappings |
| maps-spec-array-dim, used | 10.2 Dynamic Data Group Mappings |
| maps_redundantly | 4.6 Tokens |
| maps_redundantly | 10.2 Dynamic Data Group Mappings |
| Marinov | 16.2 Code Contracts |
| matching, of implemetations to model programs | 15.1 Ideas Behind Model Programs |
| max of a set of lock objects | 12.4.20 \max |
| max-expression, defined | 12.4.20 \max |
| max-expression, used | 12.4 JML Primary Expressions |
| maximum, see \max | 12.4.24.2 Generalized Quantifiers |
| meaning of expressions in JML | 2.7 Expression Evaluation and Undefinedness |
| measured by clause | 9.9.12 Measured By Clauses |
| measured-by-keyword, defined | 9.9.12 Measured By Clauses |
| measured-by-keyword, used | 9.9.12 Measured By Clauses |
| measured-clause, defined | 9.9.12 Measured By Clauses |
| measured-clause, used | Syntax |
| measured-clause, used | 15.6 Specification Statements |
| measured_by | 4.6 Tokens |
| measured_by | 9.6.2 Semantics of non-helper methods |
| measured_by | 9.9.12 Measured By Clauses |
| measured_by_redundantly | 4.6 Tokens |
| measured_by_redundantly | 9.9.12 Measured By Clauses |
| member-decl, defined | 7.1 Java Member Declarations |
| member-decl, used | 7. Class and Interface Member Declarations |
| member-field-ref, defined | 10.2 Dynamic Data Group Mappings |
| member-field-ref, used | 10.2 Dynamic Data Group Mappings |
| method | 4.6 Tokens |
| method | 7.1.1 Method and Constructor Declarations |
| method body, in separate files | 17.3 Type Checking Separate Files |
| method call, space used by | 12.4.13 \working_space |
| method calls, and invariants | 8.2 Invariants |
| method calls, and ownership typing rules | 18.6.2 Ownership Typing for Expressions |
| method declaration, in separate files | 17.3 Type Checking Separate Files |
| method refinement | 17.3 Type Checking Separate Files |
| method specification | 9. Method Specifications |
| method specification semantics, and exceptions | 9.6.2 Semantics of non-helper methods |
| method specification, omitted | Semantics |
| method, behavior of | 1.1 Behavioral Interface Specifications |
| method, helper | 7.1.1.4 Helper Methods and Constructors |
| method, model | 7.1.1.2 Model Methods and Constructors |
| method, pure | 7.1.1.3 Pure Methods and Constructors |
| method-body, defined | 7.1.1 Method and Constructor Declarations |
| method-body, used | 7.1.1 Method and Constructor Declarations |
| method-decl, defined | 7.1.1 Method and Constructor Declarations |
| method-decl, used | 7.1 Java Member Declarations |
| method-head, defined | 7.1.1 Method and Constructor Declarations |
| method-head, used | 7.1.1 Method and Constructor Declarations |
| method-name, defined | 8.3 Constraints |
| method-name, used | 8.3 Constraints |
| method-name-list, defined | 8.3 Constraints |
| method-name-list, used | 8.3 Constraints |
| method-name-list, used | 9.9.11 Callable Clauses |
| method-name-list, used | 12.4.7 \only_called |
| method-or-constructor-keyword, defined | 7.1.1 Method and Constructor Declarations |
| method-or-constructor-keyword, used | 7.1.1 Method and Constructor Declarations |
| method-ref, defined | 8.3 Constraints |
| method-ref, used | 8.3 Constraints |
| method-ref-rest, defined | 8.3 Constraints |
| method-ref-rest, used | 8.3 Constraints |
| method-ref-start, defined | 8.3 Constraints |
| method-ref-start, used | 8.3 Constraints |
| method-specification, defined | 9.2 Organization of Method Specifications |
| method-specification, in documentation comments | 4.5 Documentation Comments |
| method-specification, used | 4.5 Documentation Comments |
| method-specification, used | 7.1.1 Method and Constructor Declarations |
| method-specification, used | 7.2 Class Initializer Declarations |
| methodology, and JML | 1.3 What is JML Good For? |
| Meyer | 1.1 Behavioral Interface Specifications |
| Meyer | 1.2 A First Example |
| Meyer | 1.5 Historical Precedents |
| Meyer | 1.5 Historical Precedents |
| Meyer | 1.5 Historical Precedents |
| microsyntax | 4. Lexical Conventions |
| microsyntax, defined | 4. Lexical Conventions |
| minimum, see \min | 12.4.24.2 Generalized Quantifiers |
| model | 1.2 A First Example |
| model | 2.2 Model and Ghost |
| model | 4.6 Tokens |
| model | 5.2 Import Declarations |
| model | 5.2 Import Declarations |
| model | 6.1.2 Modifiers for Type Declarations |
| model | 6.1.2.2 Model Type Declarations |
| model | 6.2 Modifiers |
| model | 6.2.6 Model |
| model | 7.1.1.2 Model Methods and Constructors |
| model | 7.1.2.1 JML Modifiers for Fields |
| model and final | 6.2.6 Model |
| model and pure, constructors | 7.1.1.2 Model Methods and Constructors |
| model and pure, methods | 7.1.1.2 Model Methods and Constructors |
| model and static, in interfaces | 6.2.6 Model |
| model classes, vs. pure classes | 7.1.1.3 Pure Methods and Constructors |
| model constructor | 7.1.1.2 Model Methods and Constructors |
| model features | 2.2 Model and Ghost |
| model features, and namespace issues | 2.2 Model and Ghost |
| model field | 1.2 A First Example |
| model field | 2.2 Model and Ghost |
| model fields | 1.2 A First Example |
| model fields, from spec_protected | 2.4 Privacy Modifiers and Visibility |
| model fields, from spec_public | 2.4 Privacy Modifiers and Visibility |
| model fields, in interfaces | 6.2.6 Model |
| model fields, of an ADT | 1.2 A First Example |
| model import | 2.2 Model and Ghost |
| model import declaration | 5.2 Import Declarations |
| model import, vs. import | 5.2 Import Declarations |
| model method | 2.2 Model and Ghost |
| model method | 7.1.1.2 Model Methods and Constructors |
| model method, in separate files | 17.3 Type Checking Separate Files |
| model methods, vs. pure methods | 7.1.1.3 Pure Methods and Constructors |
| model program, ideas behind | 15.1 Ideas Behind Model Programs |
| model program, matching of | 15.1 Ideas Behind Model Programs |
| model program, via extract | 7.1.1 Method and Constructor Declarations |
| model type | 2.2 Model and Ghost |
| model type, vs. pure type used for modeling | 6.1.2.2 Model Type Declarations |
| model vs. ghost | 6.2.6 Model |
| model, in separate files | 17.3 Type Checking Separate Files |
| model, meaning of | 2.2 Model and Ghost |
| model, modifier in separate file | 17.3 Type Checking Separate Files |
| model, modifier in separate file | 17.3 Type Checking Separate Files |
| model, modifier in separate files | 17.3 Type Checking Separate Files |
| model, type declaration modifier | 6.1.2.2 Model Type Declarations |
| model-oriented specification | 1.1 Behavioral Interface Specifications |
| model-prog-statement, defined | 15.3 Details of Model Programs |
| model-prog-statement, used | 13. Statements and Annotation Statements |
| model-program, defined | 15.3 Details of Model Programs |
| model-program, used | 9.2 Organization of Method Specifications |
| model_program | 4.6 Tokens |
| model_program | 15.3 Details of Model Programs |
| modifiable | 4.6 Tokens |
| modifiable | 9.9.9 Assignable Clauses |
| modifiable clause | 9.9.9 Assignable Clauses |
| modifiable clause, omitted | 9.9.9 Assignable Clauses |
| modifiable_redundantly | 4.6 Tokens |
| modifiable_redundantly | 9.9.9 Assignable Clauses |
| modifier ordering, suggested | 6.2.1 Suggested Modifier Ordering |
| modifier, defined | 6.2 Modifiers |
| modifier, general description of | 6.2 Modifiers |
| modifier, pure | 6.2.5 Pure |
| modifier, used | 6.2 Modifiers |
| modifiers for bound variables | 12.4.24.5 Modifiers for Bound Variables |
| modifiers, defined | 6.2 Modifiers |
| modifiers, for classes | 6.1.2 Modifiers for Type Declarations |
| modifiers, for interfaces | 6.1.2 Modifiers for Type Declarations |
| modifiers, for type declarations | 6.1.2 Modifiers for Type Declarations |
| modifiers, Java | 6.2 Modifiers |
| modifiers, summary of | D. Modifier Summary |
| modifiers, used | 6.1 Class and Interface Declarations |
| modifiers, used | 7.1.1 Method and Constructor Declarations |
| modifiers, used | 7.1.2 Field and Variable Declarations |
| modifiers, used | 8. Type Specifications |
| modifiers, used | 13.2 Loop Statements |
| modifies | 4.6 Tokens |
| modifies | 9.9.9 Assignable Clauses |
| modifies clause | 9.9.9 Assignable Clauses |
| modifies clause, omitted | 9.9.9 Assignable Clauses |
| modifies_redundantly | 4.6 Tokens |
| modifies_redundantly | 9.9.9 Assignable Clauses |
| monitored | 4.6 Tokens |
| monitored | 6.2 Modifiers |
| monitored | 6.2.10 Monitored |
| monitored | 7.1.2.1 JML Modifiers for Fields |
| monitors-for-clause, defined | 8.9 Monitors For Clause |
| monitors-for-clause, defined | A.1.3 Deprecated Monitors For Clause Syntax |
| monitors-for-clause, used | 8. Type Specifications |
| monitors_for | 4.6 Tokens |
| monitors_for | 8.9 Monitors For Clause |
| monitors_for | A.1.3 Deprecated Monitors For Clause Syntax |
| Morgan | 1.5 Historical Precedents |
| Morgan | 15. Model Programs |
| Morris | 15. Model Programs |
| mult-expr, defined | 12.3 Expressions |
| mult-expr, used | 12.3 Expressions |
| mult-op, defined | 12.3 Expressions |
| mult-op, used | 12.3 Expressions |
| multiline comment, see C-Style comment | 4.3 Comments |
| multiple inheritance | 6.1.1 Subtyping for Type Declarations |
| multiplication, quantified, see \product | 12.4.24.2 Generalized Quantifiers |
|