| Index Entry | Section |
|---|
|
| N | | |
|---|
| Namara | Acknowledgments |
| Namara | Acknowledgments |
| new | 2.1.3.1 The Assignable Clause |
| new | 2.3.6 USMoney |
| new {|} | 3.1 Extensions to Java Expressions for Predicates |
| new, and assertions | 3.1 Extensions to Java Expressions for Predicates |
| Nielson | 3.1 Extensions to Java Expressions for Predicates |
| Nijmegen, University of | 1.3 Goals |
| Nijmegen, University of | 1.4 Tool Support |
| non-null | 2.1.2 Invariants |
| non-null elements, of an array | 3.1 Extensions to Java Expressions for Predicates |
| non_null | A. Specification Case Defaults |
| nondeterminism in exception specifications | 2.2.2.4 Pitfalls in Specifying Exceptions |
| normal termination | 2.1.3.4 Correct Implementation |
| normal_behavior | 1.1 Behavioral Interface Specification |
| normal_behavior | 2.1.3.4 Correct Implementation |
| normal_behavior, desugaring | 2.2.2.3 Multiple Specification Cases |
| normal_example | 2.3.2.1 Redundant Examples |
| NSF | Acknowledgments |
| null, protection from | 2.4 Use of Pure Classes |
| numerical quantifier, see \num_of | 3.1 Extensions to Java Expressions for Predicates |
|
| O | | |
|---|
| Ogden | 2.1.1 Model Fields |
| old | 2.3.3 MoneyComparable and MoneyOps |
| old values | 2.1.3.2 Old Values |
| old values | 3.1 Extensions to Java Expressions for Predicates |
| Oltes | Acknowledgments |
| omitted clauses in method specifications | A. Specification Case Defaults |
| omitted privacy in specification | 1.2 Lightweight Specifications |
| omitted specification, meaning of | A. Specification Case Defaults |
| omitted, assignable clause | 2.1.3.1 The Assignable Clause |
| org.jmlspecs.models package | 2.1.1 Model Fields |
| org.jmlspecs.models package | 2.3 Types For Modeling |
| overriding method, meaning of omitted specification for | A. Specification Case Defaults |
| overriding, and method specifications | 2.2.1.4 Adding to Method Specifications |
| overriding, specification of | 2.3.2.2 JMLType and Informal Predicates |
|
| P | | |
|---|
| partiality | 3.1 Extensions to Java Expressions for Predicates |
| pitfalls, in specifying exceptions | 2.2.2.4 Pitfalls in Specifying Exceptions |
| Poetzsch-Heffter | 2.1.3.4 Correct Implementation |
| Poetzsch-Heffter | 2.2.2.1 Data Groups and Represents Clauses |
| Poetzsch-Heffter | Acknowledgments |
| Poetzsch-Heffter | Acknowledgments |
| Poll | Acknowledgments |
| Poll, Erik | 2.2.2.4 Pitfalls in Specifying Exceptions |
| post, see ensures | 1.1 Behavioral Interface Specification |
| post-state | 2.1.3.1 The Assignable Clause |
| postcondition | 1.1 Behavioral Interface Specification |
| postcondition checking | 1.4.3 Run Time Assertion Checking |
| postcondition, multiple | 1.1 Behavioral Interface Specification |
| Potts | Acknowledgments |
| pre, see requires | 1.1 Behavioral Interface Specification |
| pre-state | 2.1.3.1 The Assignable Clause |
| precondition | 1.1 Behavioral Interface Specification |
| precondition checking | 1.4.3 Run Time Assertion Checking |
| preconditions, and constructors | 3.1 Extensions to Java Expressions for Predicates |
| predicates, additions to Java expressions for | 3.1 Extensions to Java Expressions for Predicates |
| predicates, Java expressions prohibited in | 3.1 Extensions to Java Expressions for Predicates |
| private | 2.2.2.1 Data Groups and Represents Clauses |
| product, see \product | 3.1 Extensions to Java Expressions for Predicates |
| protection, from undefinedness | 2.4 Use of Pure Classes |
| protection, in method specification | 2.2.1.5 Specifying Exceptional Behavior |
| protection, of precondition | 2.3.3 MoneyComparable and MoneyOps |
| prototyping from specifications | 1.3 Goals |
| public specification | 1.1 Behavioral Interface Specification |
| public, omitted | 1.2 Lightweight Specifications |
| publicly visible state | 2.1.2 Invariants |
| pure | 2.3 Types For Modeling |
| pure | A. Specification Case Defaults |
| pure class, example of | 2.5.2 ArcType |
| pure classes, use in modeling | 2.4 Use of Pure Classes |
| pure classes, vs. model classes | 2.3.1 Purity |
| pure constructor | 2.3.1 Purity |
| pure interface | 2.3.1 Purity |
| pure interface | 2.5.1 NodeType |
| pure method | 1.3 Goals |
| pure method | 2.3.1 Purity |
| pure methods, vs. model methods | 2.3.1 Purity |
| pure model method, example of | 2.3.3 MoneyComparable and MoneyOps |
| pure, example of | 2.3.3 MoneyComparable and MoneyOps |
| pure, implicit verification condition for termination | 2.3.1 Purity |
| purity | 3.1 Extensions to Java Expressions for Predicates |
| purity, and determinism | 2.3.1 Purity |
|
| Q | | |
|---|
| quantified addition, see \sum | 3.1 Extensions to Java Expressions for Predicates |
| quantified maximum, see \max | 3.1 Extensions to Java Expressions for Predicates |
| quantified minimum, see \min | 3.1 Extensions to Java Expressions for Predicates |
| quantified multiplication, see \product | 3.1 Extensions to Java Expressions for Predicates |
| quantifier, body | 3.1 Extensions to Java Expressions for Predicates |
| quantifier, generalized | 3.1 Extensions to Java Expressions for Predicates |
| quantifier, range predicate in | 3.1 Extensions to Java Expressions for Predicates |
| quantifiers | 1.3 Goals |
| quantifiers | 3.1 Extensions to Java Expressions for Predicates |
|
| R | | |
|---|
| Raghavan | 2.2.1.5 Specifying Exceptional Behavior |
| Raghavan | 2.2.1.5 Specifying Exceptional Behavior |
| Raghavan | 2.2.2.3 Multiple Specification Cases |
| Raghavan | Acknowledgments |
| Raghavan | Acknowledgments |
| range predicate, in quantifier | 3.1 Extensions to Java Expressions for Predicates |
| range predicate, not satisfiable | 3.1 Extensions to Java Expressions for Predicates |
| recursion, and pure methods | 2.3.1 Purity |
| recursion, in model methods | 2.5.3 Digraph |
| redundancy | 2.2.2.2 Redundant Specification |
| redundancy | 2.3.2.1 Redundant Examples |
| redundancy, checking | 2.2.2.2 Redundant Specification |
| redundancy, in assignable clause | 2.3.6 USMoney |
| redundant examples | 2.3.2.1 Redundant Examples |
| redundant, ensures clauses | 2.2.2.5 Redundant Ensures Clauses |
| redundantly, suffix on keywords | 2.2.2.2 Redundant Specification |
| reference semantics | 2.1.3.3 Reference Semantics |
| reference semantics, and equality | 2.1.3.3 Reference Semantics |
| reference types | 2.1.3.3 Reference Semantics |
| reference types, and equality tests | 2.1.3.3 Reference Semantics |
| refine | 1.1 Behavioral Interface Specification |
| refine | 2.2.2.3 Multiple Specification Cases |
| refinement | 1.1 Behavioral Interface Specification |
| refinement calculus | 1.3 Goals |
| refinement calculus | 1.3 Goals |
| refines | 1.4.1 Type Checking Specifications |
| `refines-java' filename suffix | 1.4.1 Type Checking Specifications |
| `refines-jml' filename suffix | 1.4.1 Type Checking Specifications |
| `refines-spec' filename suffix | 1.4.1 Type Checking Specifications |
| reflection in assertions | 3.1 Extensions to Java Expressions for Predicates |
| Reiter | 2.1.3.1 The Assignable Clause |
| release, of JML | 1.4 Tool Support |
| represents | 2.2.2.1 Data Groups and Represents Clauses |
| represents clause | 2.2.2.1 Data Groups and Represents Clauses |
| represents clause | 2.6 Behavioral Subtyping |
| represents clause | 3.2 Extensions to Java Expressions for Store-Refs |
| represents clause, and reasoning | 2.2.2.1 Data Groups and Represents Clauses |
| represents, example of | 2.3.4 MoneyAC |
| requires | 1.1 Behavioral Interface Specification |
| requires | 1.2 Lightweight Specifications |
| requires | 2.1.3.4 Correct Implementation |
| requires clauses, and constructors | 3.1 Extensions to Java Expressions for Predicates |
| requires, default for | A. Specification Case Defaults |
| RESOLVE | 2.1.1 Model Fields |
| result, of a method | 3.1 Extensions to Java Expressions for Predicates |
| returns, default for | A. Specification Case Defaults |
| reverse implication, see <== | 3.1 Extensions to Java Expressions for Predicates |
| rhetorical points | 2.2.2.2 Redundant Specification |
| Rinard | 2.3.1 Purity |
| Rioux | Acknowledgments |
| Rockwell International Corporation | Acknowledgments |
| Rodriguez | 4. Conclusions |
| Rosenblum | 1.1 Behavioral Interface Specification |
| Ruby | 2.1.3.1 The Assignable Clause |
| Ruby | 2.6 Behavioral Subtyping |
| run-time assertion checking | 1.4.3 Run Time Assertion Checking |
| runtime assertion checking | 1.4.3 Run Time Assertion Checking |
| Russell | 3.1 Extensions to Java Expressions for Predicates |
| Russell's paradox | 3.1 Extensions to Java Expressions for Predicates |
|