| Index Entry | Section |
|---|
|
| B | | |
|---|
| Büchi | 1.3 Goals |
| Büchi | Acknowledgments |
| Back | 1.3 Goals |
| Back | 1.3 Goals |
| Back | 2.1.1 Model Fields |
| Back | 2.3.6 USMoney |
| Baker | 1. Introduction |
| Baker | 1.3 Goals |
| Becker | Acknowledgments |
| behavior | 1.1 Behavioral Interface Specification |
| behavior, use in desugaring | 2.2.2.3 Multiple Specification Cases |
| behavior, vs. normal_behavior | 2.2.1.5 Specifying Exceptional Behavior |
| behavior, when to use | 2.2.1.5 Specifying Exceptional Behavior |
| behavioral interface specification language | 1.1 Behavioral Interface Specification |
| behavioral subtyping | 2.6 Behavioral Subtyping |
| benevolent side effect | 2.1.3.1 The Assignable Clause |
| Bhorkar | Acknowledgments |
| Bhorkar | Acknowledgments |
| BISL | 1. Introduction |
| blank final, and constructor specifications | 3.1 Extensions to Java Expressions for Predicates |
| body of a quantifier | 3.1 Extensions to Java Expressions for Predicates |
| Borgida | 2.1.3.1 The Assignable Clause |
| Boyland | Acknowledgments |
| Boysen | Acknowledgments |
| Boysen | Acknowledgments |
| breaks, default for | A. Specification Case Defaults |
|
| C | | |
|---|
| case analysis, nested | 2.3.2.2 JMLType and Informal Predicates |
| case analysis, nested, example of | 2.5.3 Digraph |
| Chalin | Acknowledgments |
| Chalin | Acknowledgments |
| Chan | Acknowledgments |
| Chan | Acknowledgments |
| Chan Wai Ting | Acknowledgments |
| checkable redundancy | 2.2.2.2 Redundant Specification |
| checker | 1.4 Tool Support |
| checker, for JML | 1.4.1 Type Checking Specifications |
| Chen | Acknowledgments |
| Cheon | Acknowledgments |
| Cheon | Acknowledgments |
| Cheon | Acknowledgments |
| Cheon, Yoonsik | 1.4.3 Run Time Assertion Checking |
| class for modeling, example of | 2.5.2 ArcType |
| class specification | 2. Class and Interface Specifications |
| class, model | 2.5.2 ArcType |
| classes, pure, use of | 2.4 Use of Pure Classes |
| clauses, multiple | 2.2.2.3 Multiple Specification Cases |
| client, specification for | 1.1 Behavioral Interface Specification |
| Clifton | Acknowledgments |
| Clifton | Acknowledgments |
| Clifton | Acknowledgments |
| clone | 2.2.1.4 Adding to Method Specifications |
| clone | 2.3.2.2 JMLType and Informal Predicates |
| Cohen | 3.1 Extensions to Java Expressions for Predicates |
| Cohen | 3.1 Extensions to Java Expressions for Predicates |
| Cok | Acknowledgments |
| Cok | Acknowledgments |
| Cok | Acknowledgments |
| collection model types | 2.3 Types For Modeling |
| command for checking JML files | 1.4.1 Type Checking Specifications |
| Compaq SRC | 1.3 Goals |
| Compaq SRC | 1.4 Tool Support |
| completely omitted specification | A. Specification Case Defaults |
| comprehensions, for sets | 3.1 Extensions to Java Expressions for Predicates |
| conclusions | 4. Conclusions |
| concrete fields, relating to models | 2.2 Data Groups |
| concurrency | 4. Conclusions |
| constraint | 2.2.1.2 Invariants and History Constraint |
| constructor, and preconditions | 3.1 Extensions to Java Expressions for Predicates |
| constructor, default, specification of | A. Specification Case Defaults |
| constructor, pure | 2.3.1 Purity |
| constructors, and the assignable clause | 2.3.6 USMoney |
| container classes, in JML models directory | 2.5.3 Digraph |
| continues, default for | A. Specification Case Defaults |
| contract | 1.1 Behavioral Interface Specification |
| correct implementation | 2.1.3.4 Correct Implementation |
| correctness | 2.1.3.4 Correct Implementation |
| correctness, of ADT implementation | 2.3.4 MoneyAC |
|
| D | | |
|---|
| da Costa Gomez | Acknowledgments |
| Dai | Acknowledgments |
| Daikon invariant detector | 1.4 Tool Support |
| data abstraction | 2.2.2.1 Data Groups and Represents Clauses |
| data group | 2.2.2.1 Data Groups and Represents Clauses |
| data group membership | 2.2.2.1 Data Groups and Represents Clauses |
| data groups | 2.2 Data Groups |
| data groups, and assignable clause | 2.2.2.1 Data Groups and Represents Clauses |
| data groups, and assignable clauses | 2.2.2.1 Data Groups and Represents Clauses |
| data groups, and frame axioms | 2.2.2.1 Data Groups and Represents Clauses |
| data groups, and inheritance | 2.6 Behavioral Subtyping |
| data groups, and modifies clauses | 2.2.2.1 Data Groups and Represents Clauses |
| data type induction | 2.1.1 Model Fields |
| Daugherty | Acknowledgments |
| Davies | 1.3 Goals |
| debugging, specifications | 2.2.2.2 Redundant Specification |
| default constructor, specification of | A. Specification Case Defaults |
| default privacy | 1.2 Lightweight Specifications |
| default, for requires clause | 1.2 Lightweight Specifications |
| defaults, for omitted clauses in method specifications | A. Specification Case Defaults |
| desugaring for spec_public and spec_protected | 2.1.4 Models and Lightweight Specifications |
| deterministic, pure method | 2.3.1 Purity |
| Dhara | 2.2.2.3 Multiple Specification Cases |
| Dhara | 2.6 Behavioral Subtyping |
| Dietl | Acknowledgments |
| directory, argument to jml script | 1.4.1 Type Checking Specifications |
| diverges | A. Specification Case Defaults |
| diverges, default for | A. Specification Case Defaults |
| documentation comment, specification in | 1.1 Behavioral Interface Specification |
| Docxx | Acknowledgments |
| Dooren | Acknowledgments |
| downloading, JML | 4. Conclusions |
| duration, default for | A. Specification Case Defaults |
| dynamic type of an expression | 3.1 Extensions to Java Expressions for Predicates |
| dynamic, assertion checking | 1.4.3 Run Time Assertion Checking |
|