| Index Entry | Section |
|---|
|
| J | | |
|---|
| Jacobs | 1.4 Tool Support |
| Jacobs | Acknowledgments |
| Java | 1. Introduction |
| `java' filename suffix | 1.4.1 Type Checking Specifications |
| Java Modeling Language | 1. Introduction |
| Java vs. JML assertions | 2.3.5 MoneyComparableAC |
| Java, additions to expressions | 3. Extensions to Java Expressions |
| Java, expressions prohibited in assertions | 3.1 Extensions to Java Expressions for Predicates |
| Java, failures in virtual machine | 2.1.3.4 Correct Implementation |
| `java-refined' filename suffix | 1.4.1 Type Checking Specifications |
| java.lang.Class, vs. \type() | 3.1 Extensions to Java Expressions for Predicates |
| javadoc | 1.4.2 Generating HTML Documentation |
| javadoc comments | 1.1 Behavioral Interface Specification |
| JML | 1. Introduction |
| JML | 1. Introduction |
| JML checker | 1.4 Tool Support |
| JML checker | 1.4.1 Type Checking Specifications |
| `jml' filename suffix | 1.4.1 Type Checking Specifications |
| jml script | 1.4.1 Type Checking Specifications |
| JML vs. Java assertions | 2.3.5 MoneyComparableAC |
| JML, downloading | 4. Conclusions |
| JML, web page | 4. Conclusions |
| JML, web page | 4. Conclusions |
| jml-junit script | 1.4.4 Unit Testing with JML |
| `jml-refined' filename suffix | 1.4.1 Type Checking Specifications |
| jmlc script | 1.4.3 Run Time Assertion Checking |
| jmldoc script | 1.4.2 Generating HTML Documentation |
| JMLObjectSet | 3.1 Extensions to Java Expressions for Predicates |
| jmlrac script | 1.4.3 Run Time Assertion Checking |
| jmlunit script | 1.4.4 Unit Testing with JML |
| JMLValueSet | 2.5.3 Digraph |
| JMLValueSet | 3.1 Extensions to Java Expressions for Predicates |
| Jones | 1.1 Behavioral Interface Specification |
| Jones | 1.3 Goals |
| Jonkers | 1.1 Behavioral Interface Specification |
| Jouvelot | 3.1 Extensions to Java Expressions for Predicates |
| jtest script | 1.4.4 Unit Testing with JML |
| JUnit | 1.4.4 Unit Testing with JML |
|
| K | | |
|---|
| Kiniry | Acknowledgments |
| Kiniry | Acknowledgments |
|
| L | | |
|---|
| Larch | 1.3 Goals |
| Larch | 1.3 Goals |
| Larch, differences from | 2.1.3.1 The Assignable Clause |
| Larch/C++ | 1.1 Behavioral Interface Specification |
| Larch/C++ | 1.3 Goals |
| Larsen | 1.3 Goals |
| Lea | Acknowledgments |
| Leavens | 1.1 Behavioral Interface Specification |
| Leavens | 1.3 Goals |
| Leavens | 1.3 Goals |
| Leavens | 2.1.3.1 The Assignable Clause |
| Leavens | 2.2.1.5 Specifying Exceptional Behavior |
| Leavens | 2.2.1.5 Specifying Exceptional Behavior |
| Leavens | 2.2.1.5 Specifying Exceptional Behavior |
| Leavens | 2.2.2.2 Redundant Specification |
| Leavens | 2.2.2.3 Multiple Specification Cases |
| Leavens | 2.2.2.3 Multiple Specification Cases |
| Leavens | 2.3.2.2 JMLType and Informal Predicates |
| Leavens | 2.3.3 MoneyComparable and MoneyOps |
| Leavens | 2.3.6 USMoney |
| Leavens | 2.4 Use of Pure Classes |
| Leavens | 2.6 Behavioral Subtyping |
| Leavens | 2.6 Behavioral Subtyping |
| Leino | 1.4 Tool Support |
| Leino | 2.1.3.1 The Assignable Clause |
| Leino | 2.1.3.1 The Assignable Clause |
| Leino | 2.2.2.1 Data Groups and Represents Clauses |
| Leino | 2.2.2.1 Data Groups and Represents Clauses |
| Leino | 2.3.4 MoneyAC |
| Leino | 2.3.6 USMoney |
| Leino | Acknowledgments |
| lightweight specification | 1.2 Lightweight Specifications |
| lightweight specifications | 2.1.4 Models and Lightweight Specifications |
| lightweight specifications | A. Specification Case Defaults |
| Liskov | 2.2.1.2 Invariants and History Constraint |
| local variables, and assignable clause | 2.1.3.1 The Assignable Clause |
| logic, undefinedness in | 3.1 Extensions to Java Expressions for Predicates |
| logical equivalence, see <==> | 3.1 Extensions to Java Expressions for Predicates |
| logical implication, see ==> | 3.1 Extensions to Java Expressions for Predicates |
| Loop | 1.4 Tool Support |
| Lucassen | 3.1 Extensions to Java Expressions for Predicates |
| Luckham | 1.1 Behavioral Interface Specification |
|
| M | | |
|---|
| Müller | 2.2.2.1 Data Groups and Represents Clauses |
| Müller | Acknowledgments |
| maps | 2.2.2.1 Data Groups and Represents Clauses |
| maps | 2.2.2.1 Data Groups and Represents Clauses |
| maps-into clause | 2.2.2.1 Data Groups and Represents Clauses |
| Marche | Acknowledgments |
| mathematical modeling | 1.3 Goals |
| maximum, see \max | 3.1 Extensions to Java Expressions for Predicates |
| measured_by | 2.5.3 Digraph |
| measured_by, default for | A. Specification Case Defaults |
| Mertens | Acknowledgments |
| method specification | 2.1.3 Method Specifications |
| method specification | 2.2.1.3 Details of the Method Specifications |
| method specification, addition to | 2.2.1.4 Adding to Method Specifications |
| method specification, multiple clauses in | 2.2.2.3 Multiple Specification Cases |
| method specification, omitted | A. Specification Case Defaults |
| method specifications, defaults for clauses | A. Specification Case Defaults |
| method, pure | 2.3.1 Purity |
| method, result of | 3.1 Extensions to Java Expressions for Predicates |
| Meyer | 1.1 Behavioral Interface Specification |
| Meyer | 1.3 Goals |
| Meyer | 2.2.2.5 Redundant Ensures Clauses |
| Mikhajlova | 2.3.6 USMoney |
| Millstein | Acknowledgments |
| minimum, see \min | 3.1 Extensions to Java Expressions for Predicates |
| MIT | 1.4 Tool Support |
| model | 2.1.1 Model Fields |
| model class | 2.5.2 ArcType |
| model classes | 2.1.1 Model Fields |
| model classes | 2.3 Types For Modeling |
| model classes, vs. pure classes | 2.3.1 Purity |
| model declaration | 2.1.1 Model Fields |
| model field | 2.1.1 Model Fields |
| model fields, from spec_protected | 2.1.4 Models and Lightweight Specifications |
| model fields, from spec_public | 2.1.4 Models and Lightweight Specifications |
| model fields, in interfaces | 2.2.1.1 Model Fields in Interfaces |
| model fields, inheritance of | 2.2.2 Specification of BoundedStackInterface |
| model fields, relating to concrete | 2.2 Data Groups |
| model import | 2.1.1 Model Fields |
| model method, example of | 2.3.3 MoneyComparable and MoneyOps |
| model method, example of | 2.3.5 MoneyComparableAC |
| model methods, vs. pure methods | 2.3.1 Purity |
| model types | 2.3 Types For Modeling |
| model types, for collections | 2.3 Types For Modeling |
| model types, value vs. object | 2.3 Types For Modeling |
| model variables, modification of | 2.1.3.1 The Assignable Clause |
| model, for a subtype | 2.6 Behavioral Subtyping |
| model-based specification | 1.3 Goals |
| modeling types, defining your own | 2.3 Types For Modeling |
| modeling, for ADTs, example of | 2.5 Composition for Container Classes |
| modifiable, see assignable | 2.1.3.1 The Assignable Clause |
| modification, of model variables | 2.1.3.1 The Assignable Clause |
| modified | 2.1.3.1 The Assignable Clause |
| modifies clause | 2.1.3.1 The Assignable Clause |
| modifies clauses, and data groups | 2.2.2.1 Data Groups and Represents Clauses |
| modifies, see assignable | 2.1.3.1 The Assignable Clause |
| modify, locations a method can | 2.1.3.1 The Assignable Clause |
| module | 1. Introduction |
| Morgan | 1.1 Behavioral Interface Specification |
| Morgan | 1.3 Goals |
| Morgan | 1.3 Goals |
| Morgan | 2.1.1 Model Fields |
| multiple clauses | 2.2.2.3 Multiple Specification Cases |
| multiple specification cases | 2.2.2.3 Multiple Specification Cases |
| multiple, exceptions | 2.2.2.4 Pitfalls in Specifying Exceptions |
| multiplication, quantified, see \product | 3.1 Extensions to Java Expressions for Predicates |
| Mylopoulos | 2.1.3.1 The Assignable Clause |
|