| Index Entry | Section |
|---|
|
| Q | | |
|---|
| quantified addition, see \sum | 12.4.24.2 Generalized Quantifiers |
| quantified maximum, see \max | 12.4.24.2 Generalized Quantifiers |
| quantified minimum, see \min | 12.4.24.2 Generalized Quantifiers |
| quantified multiplication, see \product | 12.4.24.2 Generalized Quantifiers |
| quantified-var-declarator, defined | 12.4.24 Quantified Expressions |
| quantified-var-declarator, used | 9.9.1.1 Forall Variable Declarations |
| quantified-var-declarator, used | 12.4.24 Quantified Expressions |
| quantified-var-declarator, used | 12.5 Set Comprehensions |
| quantified-var-decls, defined | 12.4.24 Quantified Expressions |
| quantified-var-decls, used | 12.4.24 Quantified Expressions |
| quantifier | 1.2 A First Example |
| quantifier body | 1.2 A First Example |
| quantifier, body | 12.4.24.2 Generalized Quantifiers |
| quantifier, body of | 12.4.24 Quantified Expressions |
| quantifier, defined | 12.4.24 Quantified Expressions |
| quantifier, executability of | 12.4.24.4 Executability of Quantified Expressions |
| quantifier, generalized | 12.4.24.2 Generalized Quantifiers |
| quantifier, range predicate in | 12.4.24 Quantified Expressions |
| quantifier, used | 12.4.24 Quantified Expressions |
|
| R | | |
|---|
| Raghavan | 11. Specification Inheritance |
| range predicate | 1.2 A First Example |
| range predicate, and executability of quantifiers | 12.4.24.4 Executability of Quantified Expressions |
| range predicate, in quantifier | 12.4.24 Quantified Expressions |
| range predicate, not satisfiable | 12.4.24.1 Universal and Existential Quantifiers |
| range predicate, not satisfiable | 12.4.24.2 Generalized Quantifiers |
| Ravelo, Jesus | 1.6 Acknowledgments |
| reach-expression, defined | 12.4.10 \reach |
| reach-expression, used | 12.4 JML Primary Expressions |
| reachable objects | 12.4.10 \reach |
| readable | 4.6 Tokens |
| readable | 8.7 Readable If Clauses |
| readable-if-clause, defined | 8.7 Readable If Clauses |
| readable-if-clause, used | 8. Type Specifications |
| readonly | 4.6 Tokens |
| readonly | 18. Universe Type System |
| readonly | 18.3 Readonly |
| reasons, for formal documentation | 1.3 What is JML Good For? |
| recursion, and pure methods | 7.1.1.3 Pure Methods and Constructors |
| redundant clause | 14.1 Redundant Implications and Redundantly Clauses |
| redundant implication | 14.1 Redundant Implications and Redundantly Clauses |
| redundant-spec, defined | 14. Redundancy |
| redundant-spec, used | 9.2 Organization of Method Specifications |
| redundantly | 14.1 Redundant Implications and Redundantly Clauses |
| reference semantics | 12.4.2 \old and \pre |
| reference type | 2.1 Types can be Classes and Interfaces |
| reference-type, defined | 7.1.2.2 Type-Specs |
| reference-type, used | 7.1.2.2 Type-Specs |
| reference-type, used | 7.1.2.2 Type-Specs |
| reference-type, used | 8.3 Constraints |
| reference-type, used | 9.9.4 Signals Clauses |
| reference-type, used | 9.9.5 Signals-Only Clauses |
| reference-type, used | 12.3 Expressions |
| reference-type, used | 12.4.21 \is_initialized |
| refine | A.1.5 Deprecated Refine Prefix |
| refine-keyword, defined | A.1.5 Deprecated Refine Prefix |
| refine-keyword, used | A.1.5 Deprecated Refine Prefix |
| refine-prefix, defined, deprecated | A.1.5 Deprecated Refine Prefix |
| refine-prefix, used | A.1.5 Deprecated Refine Prefix |
| RefineDemo.java | 17.4 Default Constructors and Separate Files |
| RefineDemo.jml | 17.4 Default Constructors and Separate Files |
| refinement calculus | 1.5 Historical Precedents |
| refinement calculus | 15. Model Programs |
| refinement, of model program specification | 15.1 Ideas Behind Model Programs |
| refines | A.1.5 Deprecated Refine Prefix |
| refining | 4.6 Tokens |
| refining | 13.4.3 Refining Statements |
| refining statement | 13.4.3 Refining Statements |
| refining statement | 15.1 Ideas Behind Model Programs |
| refining-statement, defined | 13.4.3 Refining Statements |
| refining-statement, used | 13.4 JML Annotation Statements |
| reflection in assertions | 12.4.18 \type |
| reflection, vs. \bigint and \real | 19. Safe Math Extensions |
| relational abstraction | 8.4 Represents Clauses |
| relational-expr, defined | 12.3 Expressions |
| relational-expr, used | 12.3 Expressions |
| rep | 4.6 Tokens |
| rep | 18. Universe Type System |
| rep | 18.2 Rep and Peer |
| rep | 18.2 Rep and Peer |
| repeated elements in syntax | 3. Syntax Notation |
| replaced syntax | A. Deprecated and Replaced Syntax |
| representation exposure | 6.1.2.1 Pure Type Declarations |
| representation exposure | 18.1 Basic Concepts of Universes |
| represents | 4.6 Tokens |
| represents | 8.4 Represents Clauses |
| represents-clause, defined | 8.4 Represents Clauses |
| represents-clause, defined | A.1.2 Deprecated Represents Clause Syntax |
| represents-clause, used | 8. Type Specifications |
| represents-keyword, defined | 8.4 Represents Clauses |
| represents-keyword, used | 8.4 Represents Clauses |
| represents-keyword, used | A.1.2 Deprecated Represents Clause Syntax |
| represents_redundantly | 4.6 Tokens |
| represents_redundantly | 8.4 Represents Clauses |
| requires | 1.2 A First Example |
| requires | 2.7 Expression Evaluation and Undefinedness |
| requires | 4.6 Tokens |
| requires | 9.6.2 Semantics of non-helper methods |
| requires | 9.6.2 Semantics of non-helper methods |
| requires | 9.9.2 Requires Clauses |
| requires clause | 1.2 A First Example |
| requires clause, omitted | 9.9.2 Requires Clauses |
| requires-clause, defined | 9.9.2 Requires Clauses |
| requires-clause, used | Syntax |
| requires-keyword, defined | 9.9.2 Requires Clauses |
| requires-keyword, used | 9.9.2 Requires Clauses |
| requires_redundantly | 4.6 Tokens |
| requires_redundantly | 9.9.2 Requires Clauses |
| resend | 4.6 Tokens |
| reserved words | 4.6 Tokens |
| reserved-ownership-modifier, defined | 18. Universe Type System |
| reserved-ownership-modifier, used | 18. Universe Type System |
| resources, specification of | 12.4.11 \duration |
| resources, specification of | 12.4.12 \space |
| resources, specification of | 12.4.13 \working_space |
| result-expression, defined | 12.4.1 \result |
| result-expression, used | 12.4 JML Primary Expressions |
| return | 4.6 Tokens |
| return | 13. Statements and Annotation Statements |
| return, carriage | 4.3 Comments |
| returns | 4.6 Tokens |
| returns | 15.6.3 Returns Clause |
| returns-clause, defined | 15.6.3 Returns Clause |
| returns-clause, used | 15.6 Specification Statements |
| returns-keyword, defined | 15.6.3 Returns Clause |
| returns-keyword, used | 15.6.3 Returns Clause |
| returns_redundantly | 4.6 Tokens |
| returns_redundantly | 15.6.3 Returns Clause |
| reverse implication, see <== | 12.6.3 Forward and Reverse Implication Operators |
| Rinard | 7.1.1.3 Pure Methods and Constructors |
| Rioux | 2.7 Expression Evaluation and Undefinedness |
| Rioux | 2.7 Expression Evaluation and Undefinedness |
| Rockwell International Corporation | 1.6 Acknowledgments |
| Rodriguez | 9.6.2 Semantics of non-helper methods |
| root ownership context | 18.1 Basic Concepts of Universes |
| Rosenblum | 1.1 Behavioral Interface Specifications |
| Ruby | 1. Introduction |
| Ruby | 1.2 A First Example |
| Ruby | 1.3 What is JML Good For? |
| Ruby | 1.3 What is JML Good For? |
| Ruby | 2.4 Privacy Modifiers and Visibility |
| Ruby | 2.4 Privacy Modifiers and Visibility |
| Ruby | 2.7 Expression Evaluation and Undefinedness |
| Ruby | 7.1.1.3 Pure Methods and Constructors |
| Ruby | 14.2 Redundant Examples |
| Ruby | 16. Specification for Subtypes |
| Ruby | 16. Specification for Subtypes |
| RuntimeException, and default signals clause | 9.9.5 Signals-Only Clauses |
|