| Index Entry | Section |
|---|
|
| M | | |
|---|
| Müeller | 2.4 Privacy Modifiers and Visibility |
| Müeller | 8.2 Invariants |
| Müller | 1.6 Acknowledgments |
| 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 | 12.2.1 Loop Invariants |
| maintaining-keyword, defined | 12.2.1 Loop Invariants |
| maintaining-keyword, used | 12.2.1 Loop Invariants |
| maintaining_redundantly | 4.6 Tokens |
| maintaining_redundantly | 12.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 | 15.2 Code Contracts |
| matching, of implemetations to model programs | 14.1 Ideas Behind Model Programs |
| max of a set of lock objects | 11.4.20 \max |
| max-expression, defined | 11.4.20 \max |
| max-expression, used | 11.4 JML Primary Expressions |
| maximum, see \max | 11.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_by | 4.6 Tokens |
| measured_by | 9.6.2 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 | 17.1 Augmenting Method Declarations |
| method body, in refinements | 16.4 Type Checking Refinements |
| method call, space used by | 11.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, refining | 16.4 Type Checking Refinements |
| method refinement | 16.4 Type Checking Refinements |
| method specification | 9. Method Specifications |
| method specification semantics, and exceptions | 9.6.2 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-body, used | 17.1 Augmenting Method 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 | 11.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 |
| method-specification, used | 17.1 Augmenting Method 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 | 11.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 Definitions |
| model | 5.2 Import Definitions |
| model | 6.1.2 Modifiers for Type Definitions |
| model | 6.1.2 Modifiers for Type Definitions |
| model | 6.2 Modifiers |
| model | 6.2.5 Model |
| model | 7.1.1.2 Model Methods and Constructors |
| model | 7.1.2.1 JML Modifiers for Fields |
| model and final | 6.2.5 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.5 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.5 Model |
| model fields, of an ADT | 1.2 A First Example |
| model import | 2.2 Model and Ghost |
| model import definition | 5.2 Import Definitions |
| model import, vs. import | 5.2 Import Definitions |
| model method | 2.2 Model and Ghost |
| model method | 7.1.1.2 Model Methods and Constructors |
| model method, in refinements | 16.4 Type Checking Refinements |
| model methods, vs. pure methods | 7.1.1.3 Pure Methods and Constructors |
| model program, ideas behind | 14.1 Ideas Behind Model Programs |
| model program, matching of | 14.1 Ideas Behind Model Programs |
| model program, via extract | 7.1.1 Method and Constructor Declarations |
| model type | 2.2 Model and Ghost |
| model vs. ghost | 6.2.5 Model |
| model, in refinements | 16.4 Type Checking Refinements |
| model, meaning of | 2.2 Model and Ghost |
| model, modifier in refinement | 16.4 Type Checking Refinements |
| model, modifier in refinement | 16.4 Type Checking Refinements |
| model, modifier in refinement | 16.4 Type Checking Refinements |
| model, type definition modifier | 6.1.2 Modifiers for Type Definitions |
| model-oriented specification | 1.1 Behavioral Interface Specifications |
| model-prog-statement, defined | 14.3 Details of Model Programs |
| model-prog-statement, used | 12. Statements and Annotation Statements |
| model-program, defined | 14.3 Details of Model Programs |
| model-program, used | 9.2 Organization of Method Specifications |
| model_program | 4.6 Tokens |
| model_program | 14.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.4 Pure |
| modifier, used | 6.2 Modifiers |
| modifiers for bound variables | 11.4.24.5 Modifiers for Bound Variables |
| modifiers, defined | 6.2 Modifiers |
| modifiers, for classes | 6.1.2 Modifiers for Type Definitions |
| modifiers, for interfaces | 6.1.2 Modifiers for Type Definitions |
| modifiers, for type definitions | 6.1.2 Modifiers for Type Definitions |
| modifiers, Java | 6.2 Modifiers |
| modifiers, summary of | B. Modifier Summary |
| modifiers, used | 6.1 Class and Interface Definitions |
| 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 | 17.1 Augmenting Method Declarations |
| 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.9 Monitored |
| monitored | 7.1.2.1 JML Modifiers for Fields |
| monitors-for-clause, defined | 8.9 Monitors For Clause |
| monitors-for-clause, used | 8. Type Specifications |
| monitors_for | 4.6 Tokens |
| monitors_for | 8.9 Monitors For Clause |
| Morgan | 1.5 Historical Precedents |
| Morgan | 14. Model Programs |
| Morris | 14. Model Programs |
| Mueller | 4.6 Tokens |
| Mueller | 5. Compilation Units |
| Mueller | 18. Universe Type System |
| mult-expr, defined | 11.3 Expressions |
| mult-expr, used | 11.3 Expressions |
| mult-op, defined | 11.3 Expressions |
| mult-op, used | 11.3 Expressions |
| MultiJava | 1.4 Status and Plans for JML |
| MultiJava | 4.6 Tokens |
| MultiJava | 5. Compilation Units |
| MultiJava | 6.1.1 Subtyping for Type Definitions |
| MultiJava | 17. MultiJava Extensions to JML |
| multijava-param-declaration, defined | 17.2 MultiMethods |
| multijava-param-declaration, used | 7.1.1.1 Formal Parameters |
| multijava-separator, defined | 4.6 Tokens |
| multijava-separator, used | 4.6 Tokens |
| multijava-top-level-declaration, defined | 17.1 Augmenting Method Declarations |
| multijava-top-level-declaration, used | 5. Compilation Units |
| multijava-top-level-method, defined | 17.1 Augmenting Method Declarations |
| multijava-top-level-method, used | 17.1 Augmenting Method Declarations |
| multiline comment, see C-Style comment | 4.3 Comments |
| multimethods | 17.2 MultiMethods |
| multiple dispatch | 17.2 MultiMethods |
| multiple inheritance | 6.1.1 Subtyping for Type Definitions |
| multiplication, quantified, see \product | 11.4.24.2 Generalized Quantifiers |
|