| Index Entry | Section |
|---|
|
| O | | |
|---|
| object invariant, alternative terms for | 8.2.1 Static vs. instance invariants |
| octal-digit, defined | 4.6 Tokens |
| octal-digit, used | 4.6 Tokens |
| octal-escape, defined | 4.6 Tokens |
| octal-escape, used | 4.6 Tokens |
| octal-integer-literal, defined | 4.6 Tokens |
| octal-integer-literal, used | 4.6 Tokens |
| octal-numeral, defined | 4.6 Tokens |
| octal-numeral, used | 4.6 Tokens |
| old | 4.6 Tokens |
| old | 9.6.2 Semantics of non-helper methods |
| old | 9.6.2 Semantics of non-helper methods |
| old | 9.9.1.2 Old Variable Declarations |
| old-expression | 12.4.2 \old and \pre |
| old-expression, defined | 12.4.2 \old and \pre |
| old-expression, used | 12.4 JML Primary Expressions |
| old-var-declarator, defined | 9.9.1.2 Old Variable Declarations |
| old-var-declarator, used | 9.9.1.2 Old Variable Declarations |
| old-var-decls, defined | 9.9.1.2 Old Variable Declarations |
| old-var-decls, used | 9.9.1 Specification Variable Declarations |
| omitted specification, meaning of | Semantics |
| only-accessed-expression, defined | 12.4.5 \only_accessed |
| only-assigned-expression, defined | 12.4.6 \only_assigned |
| only-called-expression, defined | 12.4.7 \only_called |
| only-captured-expression, defined | 12.4.8 \only_captured |
| operation | 1.5 Historical Precedents |
| operator precedence | 12.3 Expressions |
| operator, of LSL | 1.5 Historical Precedents |
| operators, added to JML | 12.6 JML Operators |
| optional elements in syntax | 3. Syntax Notation |
| or | 4.6 Tokens |
| or | 15.4 Nondeterministic Choice Statement |
| or | 15.5 Nondeterministic If Statement |
| overriding method, meaning of omitted specification for | Semantics |
| overriding methods, and pure | 6.1.2.1 Pure Type Declarations |
| owner | 18.1 Basic Concepts of Universes |
| owner-as-modifier property | 18.1 Basic Concepts of Universes |
| ownership | 8.2 Invariants |
| ownership context | 18.1 Basic Concepts of Universes |
| ownership context, root | 18.1 Basic Concepts of Universes |
| ownership modifiers for array types | 18.4 Ownership Modifiers for Array Types |
| ownership modifiers for types, defaults | 18.5 Default Ownership Modifiers |
| ownership types and type checking | 18.6.2 Ownership Typing for Expressions |
| ownership types, and subtyping | 18.6.1 Ownership Subtyping |
| ownership-modifier, defined | 18. Universe Type System |
| ownership-modifier, used | 13.1.1 Modifiers for Local Declarations |
| ownership-modifier, used | 18. Universe Type System |
| ownership-modifiers, defined | 18. Universe Type System |
| ownership-modifiers, used | 7.1.2.2 Type-Specs |
|
| P | | |
|---|
| package | 4.6 Tokens |
| package | 5.1 Package Declarations |
| package declaration, satisfaction of | 5.1 Package Declarations |
| package declarations | 5.1 Package Declarations |
| package visibility | 2.4 Privacy Modifiers and Visibility |
| package-declaration, defined | 5.1 Package Declarations |
| package-declaration, used | 5. Compilation Units |
| paragraph-tag, defined | 4.5 Documentation Comments |
| paragraph-tag, used | 4.5 Documentation Comments |
| param-declaration, defined | 7.1.1.1 Formal Parameters |
| param-declaration, used | 7.1.1.1 Formal Parameters |
| param-declaration, used | 13. Statements and Annotation Statements |
| param-declaration-list, defined | 7.1.1.1 Formal Parameters |
| param-declaration-list, used | 7.1.1.1 Formal Parameters |
| param-disambig, defined | 8.3 Constraints |
| param-disambig, used | 8.3 Constraints |
| param-disambig-list, defined | 8.3 Constraints |
| param-disambig-list, used | 8.3 Constraints |
| param-modifier, defined | 7.1.1.1 Formal Parameters |
| param-modifier, used | 7.1.1.1 Formal Parameters |
| Parnas | 1.5 Historical Precedents |
| parsing | 1.3 What is JML Good For? |
| partial correctness | 9.9.7 Diverges Clauses |
| peer | 4.6 Tokens |
| peer | 18. Universe Type System |
| peer | 18.2 Rep and Peer |
| peer | 18.2 Rep and Peer |
| plans, for JML | 1.4 Status and Plans for JML |
| Poetzsch-Heffter | 1.6 Acknowledgments |
| Poetzsch-Heffter | 8.2 Invariants |
| Poetzsch-Heffter | 8.2 Invariants |
| Poetzsch-Heffter | 8.2 Invariants |
| Poetzsch-Heffter | 18. Universe Type System |
| Poetzsch-Heffter | 18.1 Basic Concepts of Universes |
| Poetzsch-Heffter | 18.1 Basic Concepts of Universes |
| Poll | 1.3 What is JML Good For? |
| portability, and language levels | 2.9 Language Levels |
| positive key | 4.4 Annotation Markers |
| positive-key, defined | 4.4 Annotation Markers |
| positive-key, used | 4.4 Annotation Markers |
| possibly-annotated-loop, defined | 13.2 Loop Statements |
| possibly-annotated-loop, used | 13. Statements and Annotation Statements |
| post | 4.6 Tokens |
| post | 9.9.3 Ensures Clauses |
| post-state | 9.6.2 Semantics of non-helper methods |
| post_redundantly | 4.6 Tokens |
| post_redundantly | 9.9.3 Ensures Clauses |
| postcondition | 1.1 Behavioral Interface Specifications |
| postcondition | 1.2 A First Example |
| postcondition | 1.5 Historical Precedents |
| postcondition, exceptional | 1.1 Behavioral Interface Specifications |
| postcondition, exceptional | 9.9.4 Signals Clauses |
| postcondition, exceptional | 9.9.5 Signals-Only Clauses |
| postcondition, normal | 1.1 Behavioral Interface Specifications |
| postcondition, normal | 9.9.3 Ensures Clauses |
| postcondition, via non_null | 7.1.1 Method and Constructor Declarations |
| postfix-expr, defined | 12.3 Expressions |
| postfix-expr, used | 12.3 Expressions |
| postfix-expr, used | 12.5 Set Comprehensions |
| Potter | 8.2 Invariants |
| Potter | 18.1 Basic Concepts of Universes |
| pre | 4.6 Tokens |
| pre | 9.9.2 Requires Clauses |
| pre-state | 9.6.2 Semantics of non-helper methods |
| pre_redundantly | 4.6 Tokens |
| pre_redundantly | 9.9.2 Requires Clauses |
| precedence, table of | 12.3 Expressions |
| precondition | 1.1 Behavioral Interface Specifications |
| precondition | 1.1 Behavioral Interface Specifications |
| precondition | 1.2 A First Example |
| precondition | 1.5 Historical Precedents |
| precondition | 9.9.2 Requires Clauses |
| precondition, protective | 2.7 Expression Evaluation and Undefinedness |
| pred-or-not, defined | 9.9.2 Requires Clauses |
| pred-or-not, used | 9.9.2 Requires Clauses |
| pred-or-not, used | 9.9.3 Ensures Clauses |
| pred-or-not, used | 9.9.4 Signals Clauses |
| pred-or-not, used | 9.9.7 Diverges Clauses |
| pred-or-not, used | 15.6.1 Continues Clause |
| pred-or-not, used | 15.6.2 Breaks Clause |
| pred-or-not, used | 15.6.3 Returns Clause |
| predicate | 12.1 Predicates |
| predicate, defined | 12.1 Predicates |
| predicate, used | 8.2 Invariants |
| predicate, used | 8.3 Constraints |
| predicate, used | 8.4 Represents Clauses |
| predicate, used | 8.5 Initially Clauses |
| predicate, used | 8.6 Axioms |
| predicate, used | 8.7 Readable If Clauses |
| predicate, used | 8.8 Writable If Clauses |
| predicate, used | 9.9.12 Measured By Clauses |
| predicate, used | 9.9.14 Working Space Clauses |
| predicate, used | 9.9.15 Duration Clauses |
| predicate, used | 12.4.24 Quantified Expressions |
| predicate, used | 12.5 Set Comprehensions |
| predicate, used | 13.2.1 Loop Invariants |
| predicate, used | 13.3 Assert Statements |
| predicate, used | 13.4.1 Assume Statements |
| predicate, used | 13.4.6 Hence By Statements |
| predicates, and exceptions | 2.7 Expression Evaluation and Undefinedness |
| preserving, an invariant | 8.2 Invariants |
| primary-expr, defined | 12.3 Expressions |
| primary-expr, used | 12.3 Expressions |
| primary-suffix, defined | 12.3 Expressions |
| primary-suffix, used | 12.3 Expressions |
| primitive value type | 2.1 Types can be Classes and Interfaces |
| privacy | Syntax |
| privacy modifiers | 2.4 Privacy Modifiers and Visibility |
| privacy, defined | 9.3 Access Control in Specification Cases |
| privacy, used | Syntax |
| privacy, used | 9.7 Normal Behavior Specification Cases |
| privacy, used | 9.8 Exceptional Behavior Specification Cases |
| privacy, used | 14.2 Redundant Examples |
| privacy, used | 15.3 Details of Model Programs |
| privacy, used | 15.6 Specification Statements |
| PrivacyDemoIllegal | 2.4 Privacy Modifiers and Visibility |
| PrivacyDemoLegalAndIllegal | 2.4 Privacy Modifiers and Visibility |
| private | 1.3 What is JML Good For? |
| private | 2.4 Privacy Modifiers and Visibility |
| private | 4.6 Tokens |
| private | 6.2 Modifiers |
| private | 9.3 Access Control in Specification Cases |
| private, and helper | 6.2.9 Helper |
| private, modifier in separate file | 17.3 Type Checking Separate Files |
| private, modifier in separate file | 17.3 Type Checking Separate Files |
| procedure claims | 14.1 Redundant Implications and Redundantly Clauses |
| product, see \product | 12.4.24.2 Generalized Quantifiers |
| programming method, and JML | 1.3 What is JML Good For? |
| protected | 2.4 Privacy Modifiers and Visibility |
| protected | 4.6 Tokens |
| protected | 6.2 Modifiers |
| protected | 9.3 Access Control in Specification Cases |
| protected, modifier in separate file | 17.3 Type Checking Separate Files |
| protected, modifier in separate file | 17.3 Type Checking Separate Files |
| protective specifications | 2.7 Expression Evaluation and Undefinedness |
| public | 1.2 A First Example |
| public | 1.3 What is JML Good For? |
| public | 2.4 Privacy Modifiers and Visibility |
| public | 4.6 Tokens |
| public | 6.2 Modifiers |
| public | 9.3 Access Control in Specification Cases |
| public specification | 1.2 A First Example |
| public type, in a compilation unit | 5. Compilation Units |
| public, modifier in separate file | 17.3 Type Checking Separate Files |
| public, modifier in separate file | 17.3 Type Checking Separate Files |
| pure | 1.2 A First Example |
| pure | 4.6 Tokens |
| pure | 4.6 Tokens |
| pure | 6.1.2 Modifiers for Type Declarations |
| pure | 6.1.2.1 Pure Type Declarations |
| pure | 6.2 Modifiers |
| pure | 6.2.5 Pure |
| pure | 7.1.1.3 Pure Methods and Constructors |
| pure | Semantics |
| pure and model, constructors | 7.1.1.2 Model Methods and Constructors |
| pure and model, methods | 7.1.1.2 Model Methods and Constructors |
| pure and void methods | 7.1.1.3 Pure Methods and Constructors |
| pure classes, vs. model classes | 7.1.1.3 Pure Methods and Constructors |
| pure constructor | 7.1.1.3 Pure Methods and Constructors |
| pure interface | 7.1.1.3 Pure Methods and Constructors |
| pure method | 7.1.1.3 Pure Methods and Constructors |
| pure methods, default ownership modifiers for parameter types of | 18.5 Default Ownership Modifiers |
| pure methods, vs. model methods | 7.1.1.3 Pure Methods and Constructors |
| pure type used for modeling, vs. model type. | 6.1.2.2 Model Type Declarations |
| pure, and overriding methods | 6.1.2.1 Pure Type Declarations |
| pure, implicit verification condition for termination | 7.1.1.3 Pure Methods and Constructors |
| pure, modifier in separate file | 17.3 Type Checking Separate Files |
| pure, type declaration modifier | 6.1.2.1 Pure Type Declarations |
| pure, vs. immutable objects | 6.1.2.1 Pure Type Declarations |
| purity, and determinism | 7.1.1.3 Pure Methods and Constructors |
| purpose, of this reference manual | 1. Introduction |
|