| Index Entry | Section |
|---|
|
| E | | |
|---|
| E | 4.6 Tokens |
| e | 4.6 Tokens |
| Eiffel | 1.1 Behavioral Interface Specifications |
| Eiffel | 1.5 Historical Precedents |
| element type, of array, expression | 11.4.17 \elemtype |
| elemtype-expression, defined | 11.4.17 \elemtype |
| elemtype-expression, used | 11.4 JML Primary Expressions |
| else | 4.6 Tokens |
| else | 12. Statements and Annotation Statements |
| else | 14.5 Nondeterministic If Statement |
| empty range | 11.4.24.1 Universal and Existential Quantifiers |
| empty range | 11.4.24.2 Generalized Quantifiers |
| end-jml-tag, defined | 4.5 Documentation Comments |
| end-jml-tag, used | 4.5 Documentation Comments |
| end-of-line, defined | 4.1 White Space |
| end-of-line, used | 4.1 White Space |
| end-of-line, used | 4.3 Comments |
| end-of-line, used | 4.5 Documentation Comments |
| ensures | 1.2 A First Example |
| ensures | 4.6 Tokens |
| ensures | 9.6.2 Non-helper methods |
| ensures | 9.6.2 Non-helper methods |
| ensures | 9.9.3 Ensures Clauses |
| ensures clause | 1.2 A First Example |
| ensures clause, omitted | 9.9.3 Ensures Clauses |
| ensures-clause, defined | 9.9.3 Ensures Clauses |
| ensures-clause, used | Syntax |
| ensures-clause, used | 14.6 Specification Statements |
| ensures-keyword, defined | 9.9.3 Ensures Clauses |
| ensures-keyword, used | 9.9.3 Ensures Clauses |
| ensures_redundantly | 4.6 Tokens |
| ensures_redundantly | 9.9.3 Ensures Clauses |
| equality-expr, defined | 11.3 Expressions |
| equality-expr, used | 11.3 Expressions |
| equivalence-expr, defined | 11.3 Expressions |
| equivalence-expr, used | 11.3 Expressions |
| equivalence-op, defined | 11.3 Expressions |
| equivalence-op, used | 11.3 Expressions |
| Ernst | 1.3 What is JML Good For? |
| Errors and method semantics | 9.6.2 Non-helper methods |
| ESC/Java | 1. Introduction |
| ESC/Java | 1.3 What is JML Good For? |
| ESC/Java | 2.4 Privacy Modifiers and Visibility |
| ESC/Java | 4.4 Annotation Markers |
| ESC/Java | 11.4.19 \lockset |
| ESC/Java | 11.4.20 \max |
| ESC/Java, differences from JML | E.1 Differences Between JML and Other Tools |
| ESC/Java2 | 2.4 Privacy Modifiers and Visibility |
| ESC/Java2 | 4.4 Annotation Markers |
| ESC/Java2, differences from JML | E.1 Differences Between JML and Other Tools |
| escape-sequence, defined | 4.6 Tokens |
| escape-sequence, used | 4.6 Tokens |
| establishing, an invariant | 8.2 Invariants |
| example | 4.6 Tokens |
| example | 13.2 Redundant Examples |
| example, defaults for | 13.2 Redundant Examples |
| example, defined | 13.2 Redundant Examples |
| example, heavyweight | 13.2 Redundant Examples |
| example, lightweight | 13.2 Redundant Examples |
| example, used | 13.2 Redundant Examples |
| example, used | 13.2 Redundant Examples |
| examples, checking | 13.2 Redundant Examples |
| examples, defined | 13.2 Redundant Examples |
| examples, meaning | 13.2 Redundant Examples |
| examples, semantics | 13.2 Redundant Examples |
| examples, specification of | 13.2 Redundant Examples |
| examples, used | 13. Redundancy |
| exceptional postcondition | 9.9.4 Signals Clauses |
| exceptional postcondition | 9.9.5 Signals-Only Clauses |
| exceptional-behavior-keyword, defined | 9.8 Exceptional Behavior Specification Cases |
| exceptional-behavior-keyword, used | 14.6 Specification Statements |
| exceptional-behavior-spec-case, defined | 9.8 Exceptional Behavior Specification Cases |
| exceptional-behavior-spec-case, used | 9.5 Heavyweight Specification Cases |
| exceptional-example-body, defined | 13.2 Redundant Examples |
| exceptional-example-body, used | 13.2 Redundant Examples |
| exceptional-spec-case, defined | 9.8 Exceptional Behavior Specification Cases |
| exceptional-spec-case, used | 9.8 Exceptional Behavior Specification Cases |
| exceptional-spec-case, used | 14.6 Specification Statements |
| exceptional-spec-clause, used | 13.2 Redundant Examples |
| exceptional_behavior | 2.3 Lightweight and Heavyweight Specifications |
| exceptional_behavior | 4.6 Tokens |
| exceptional_behavior | 9.8 Exceptional Behavior Specification Cases |
| exceptional_behavior | 9.8 Exceptional Behavior Specification Cases |
| exceptional_behaviour | 4.6 Tokens |
| exceptional_behaviour | 9.8 Exceptional Behavior Specification Cases |
| exceptional_example | 4.6 Tokens |
| exceptional_example | 13.2 Redundant Examples |
| exceptional_example, used | 13.2 Redundant Examples |
| exceptions in assertions | 2.7 Expression Evaluation and Undefinedness |
| exceptions, and method specification semantics | 9.6.2 Non-helper methods |
| exceptions, avoiding in assertion evaluation | 2.7 Expression Evaluation and Undefinedness |
| exceptions, prohibiting | 1.2 A First Example |
| exceptions, specifying when they must be thrown | 9.9.5 Signals-Only Clauses |
| exclusive-or-expr, defined | 11.3 Expressions |
| exclusive-or-expr, used | 11.3 Expressions |
| executability of quantified expressions | 11.4.24.4 Executability of Quantified Expressions |
| experimental, features of JML | 2.9 Language Levels |
| explicitly nullable | 6.2.12 Nullity Modifiers |
| exponent-indicator, defined | 4.6 Tokens |
| exponent-indicator, used | 4.6 Tokens |
| exponent-part, defined | 4.6 Tokens |
| exponent-part, used | 4.6 Tokens |
| expression | 11.3 Expressions |
| expression, boolean-valued | 11.1 Predicates |
| expression, defined | 11.3 Expressions |
| expression, used | 7.1.2 Field and Variable Declarations |
| expression, used | 11.2 Specification Expressions |
| expression, used | 11.3 Expressions |
| expression, used | 11.4.11 \duration |
| expression, used | 11.4.13 \working_space |
| expression, used | 12. Statements and Annotation Statements |
| expression, used | 12.2 Loop Statements |
| expression, used | 12.3 Assert Statements |
| expression, used | 12.4.1 Assume Statements |
| expression, used | 12.4.5 Debug Statements |
| expression, used | 17.2 MultiMethods |
| expression-list, defined | 11.3 Expressions |
| expression-list, used | 11.3 Expressions |
| expression-list, used | 12.2 Loop Statements |
| expressions, and exceptions | 2.7 Expression Evaluation and Undefinedness |
| expressions, precedence of | 11.3 Expressions |
| expressions, semantics in JML | 2.7 Expression Evaluation and Undefinedness |
| exsures | 4.6 Tokens |
| exsures | 9.9.4 Signals Clauses |
| exsures clause, default for | 9.9.4 Signals Clauses |
| exsures clause, omitted | 9.9.4 Signals Clauses |
| exsures_redundantly | 4.6 Tokens |
| exsures_redundantly | 9.9.4 Signals Clauses |
| extending-method-head, defined | 17.1 Augmenting Method Declarations |
| extending-method-head, used | 17.1 Augmenting Method Declarations |
| extending-specification, defined | 9.2 Organization of Method Specifications |
| extending-specification, used | 9.2 Organization of Method Specifications |
| extends | 4.6 Tokens |
| extends | 6.1.1 Subtyping for Type Definitions |
| extends, for classes | 6.1.1 Subtyping for Type Definitions |
| extends, for interfaces | 6.1.1 Subtyping for Type Definitions |
| extension of interfaces | 6.1.1 Subtyping for Type Definitions |
| extract | 4.6 Tokens |
| extract | 6.2 Modifiers |
| extract | 14.2 Extracting Model Program Specifications |
| extract, in method declaration | 7.1.1 Method and Constructor Declarations |
|