| Index Entry | Section |
|---|
|
| E | | |
|---|
| Edwards | Acknowledgments |
| Eiffel | 1.3 Goals |
| Eiffel | 1.3 Goals |
| Eiffel | 2.1.3.1 The Assignable Clause |
| Eiffel | 2.1.3.2 Old Values |
| element type, see \elemtype | 3.1 Extensions to Java Expressions for Predicates |
| empty range | 3.1 Extensions to Java Expressions for Predicates |
| ensures | 1.1 Behavioral Interface Specification |
| ensures | 2.1.3.4 Correct Implementation |
| ensures clause, meaning of multiple | 2.2.2.3 Multiple Specification Cases |
| ensures, default for | A. Specification Case Defaults |
| ensures, multiple | 1.1 Behavioral Interface Specification |
| ensures_redundantly | 2.2.2.5 Redundant Ensures Clauses |
| equality, guidelines for comparing | 2.1.3.3 Reference Semantics |
| equals | 2.3.2.2 JMLType and Informal Predicates |
| equals, vs. == | 2.1.3.3 Reference Semantics |
| equals, vs. == | 2.1.3.3 Reference Semantics |
| equivalence, see <==> | 3.1 Extensions to Java Expressions for Predicates |
| Ernst | 1.4 Tool Support |
| Ernst | Acknowledgments |
| error, in Java virtual machine | 2.1.3.4 Correct Implementation |
| ESC/Java | 1.2 Lightweight Specifications |
| ESC/Java | 1.3 Goals |
| ESC/Java | 2.1.3.1 The Assignable Clause |
| ESC/Java | 2.3.6 USMoney |
| ESC/Java, goals | 1.4 Tool Support |
| example | 2.3.2.1 Redundant Examples |
| examples, checking | 2.3.2.1 Redundant Examples |
| examples, in method specifications | 2.3.2.1 Redundant Examples |
| exceptional_behavior | 2.2.1.5 Specifying Exceptional Behavior |
| exceptional_behavior | 2.2.2.4 Pitfalls in Specifying Exceptions |
| exceptional_behavior, desugaring | 2.2.2.3 Multiple Specification Cases |
| exceptional_example | 2.3.2.1 Redundant Examples |
| exceptions, in expressions | 3.1 Extensions to Java Expressions for Predicates |
| exceptions, prohibiting others | 2.2.1.5 Specifying Exceptional Behavior |
| exceptions, semantics of signals clauses | 2.2.1.5 Specifying Exceptional Behavior |
| exceptions, specification of | 2.2.1.5 Specifying Exceptional Behavior |
| exceptions, specification of | 2.2.2.4 Pitfalls in Specifying Exceptions |
| exceptions, specifying details of | 2.2.2.3 Multiple Specification Cases |
| existential quantifier, see \exists | 3.1 Extensions to Java Expressions for Predicates |
| expressions, additions to Java | 3. Extensions to Java Expressions |
| expressions, in assertions | 1.1 Behavioral Interface Specification |
| exsures, see signals | 2.2.1.5 Specifying Exceptional Behavior |
|
| F | | |
|---|
| field, private | 2.6 Behavioral Subtyping |
| fields of an object | 3.2 Extensions to Java Expressions for Store-Refs |
| fields, of an ADT | 2.2 Data Groups |
| filename suffixes | 1.4.1 Type Checking Specifications |
| files, for annotations | 1.1 Behavioral Interface Specification |
| finiteness constraints | 2.1.3.4 Correct Implementation |
| Finney | 1.3 Goals |
| Fitzgerald | 1.3 Goals |
| Fleck | Acknowledgments |
| for_example | 2.3.2.1 Redundant Examples |
| formal parameters, and assignable clause | 2.1.3.1 The Assignable Clause |
| formality, escape from | 2.3.2.2 JMLType and Informal Predicates |
| frame axiom | 2.1.3.1 The Assignable Clause |
| frame axiom, see assignable clause | 2.1.3.1 The Assignable Clause |
| frame axioms, and data groups | 2.2.2.1 Data Groups and Represents Clauses |
| fresh predicate | 3.1 Extensions to Java Expressions for Predicates |
| future work | 4. Conclusions |
|
| G | | |
|---|
| Ganapathy | Acknowledgments |
| Ganapathy | Acknowledgments |
| generalized quantifier | 3.1 Extensions to Java Expressions for Predicates |
| Gifford | 3.1 Extensions to Java Expressions for Predicates |
| goals, of JML | 1. Introduction |
| goals, of JML | 1.3 Goals |
| Gosling | 1. Introduction |
| Gries | 3.1 Extensions to Java Expressions for Predicates |
| Guttag | 1.1 Behavioral Interface Specification |
| Guttag | 1.3 Goals |
|
| H | | |
|---|
| Hayes | 1.3 Goals |
| heavyweight specification | 1.2 Lightweight Specifications |
| heavyweight specifications | A. Specification Case Defaults |
| helper | 2.1.2 Invariants |
| hiding concrete fields, in specifications | 2.2.2.1 Data Groups and Represents Clauses |
| history constraint | 2.2.1.2 Invariants and History Constraint |
| history constraint, and inheritance | 2.6 Behavioral Subtyping |
| history constraint, example of | 2.3.2 Money |
| Hoare | 1.1 Behavioral Interface Specification |
| Hoare | 2.1.1 Model Fields |
| Hoare | 2.2.2.1 Data Groups and Represents Clauses |
| Hoare | 2.3.4 MoneyAC |
| Hoech | Acknowledgments |
| Holmes | 1. Introduction |
| Holmes | 1. Introduction |
| Horning | 1.1 Behavioral Interface Specification |
| Horning | 1.3 Goals |
| HTML documentation | 1.4.2 Generating HTML Documentation |
| Huisman | 1.4 Tool Support |
| Huisman | Acknowledgments |
| hypertext, generation from JML specifications | 1.4.2 Generating HTML Documentation |
|
| I | | |
|---|
| if | 2.2.2.3 Multiple Specification Cases |
| if and only if, see <==> | 3.1 Extensions to Java Expressions for Predicates |
| iff, see <==> | 3.1 Extensions to Java Expressions for Predicates |
| immutable types, defining your own | 2.3 Types For Modeling |
| implementation, correctness of | 2.3.4 MoneyAC |
| implication | 2.2.2.5 Redundant Ensures Clauses |
| implication, see ==> | 3.1 Extensions to Java Expressions for Predicates |
| implications section, of method specification | 2.2.2.3 Multiple Specification Cases |
| implications, of a specification | 2.2.2.2 Redundant Specification |
| implies_that | 2.2.2.3 Multiple Specification Cases |
| implies_that, example of | 2.3.2.2 JMLType and Informal Predicates |
| in | 2.2.2.1 Data Groups and Represents Clauses |
| in | 2.2.2.1 Data Groups and Represents Clauses |
| in clause | 2.2.2.1 Data Groups and Represents Clauses |
| in, example of | 2.3.4 MoneyAC |
| inequivalence, see <=!=> | 3.1 Extensions to Java Expressions for Predicates |
| informal descriptions | 3.1 Extensions to Java Expressions for Predicates |
| informal predicate, example of | 2.3.6 USMoney |
| informal predicates | 2.3.2.2 JMLType and Informal Predicates |
| informality | 2.3.2.2 JMLType and Informal Predicates |
| information hiding | 2.2.2.1 Data Groups and Represents Clauses |
| inheritance | 2.2.2.1 Data Groups and Represents Clauses |
| inheritance, of instance fields | 2.2.2 Specification of BoundedStackInterface |
| inheritance, of method specifications | 2.2.1.4 Adding to Method Specifications |
| inheritance, of specifications | 2.6 Behavioral Subtyping |
| initialization, in constructors | 2.3.6 USMoney |
| initially | 2.1.1 Model Fields |
| initially, and inheritance | 2.6 Behavioral Subtyping |
| instance | 2.2.1.1 Model Fields in Interfaces |
| instance | 2.2.2 Specification of BoundedStackInterface |
| instance, history constraint | 2.2.1.2 Invariants and History Constraint |
| instance, invariant | 2.2.1.2 Invariants and History Constraint |
| interface specification | 1.1 Behavioral Interface Specification |
| interface specification | 2. Class and Interface Specifications |
| interface, of a module | 1.1 Behavioral Interface Specification |
| interface, pure | 2.5.1 NodeType |
| invariant | 2.1.2 Invariants |
| invariant | 2.2.1.2 Invariants and History Constraint |
| invariant checking | 1.4.3 Run Time Assertion Checking |
| invariant, and inheritance | 2.6 Behavioral Subtyping |
| invariant, example of | 2.4 Use of Pure Classes |
| invariant, private | 2.6 Behavioral Subtyping |
| invariant, redundant | 2.2.2.2 Redundant Specification |
| invariant_redundantly | 2.2.2.2 Redundant Specification |
| Iowa State University, Com S 362 | Acknowledgments |
| Iowa State, release of JML | 1.4 Tool Support |
| Iowa, University of | Acknowledgments |
| isAssignableFrom, method of java.lang.Class | 3.1 Extensions to Java Expressions for Predicates |
| ISO | 1.3 Goals |
| ISU, Com S 362 | Acknowledgments |
|