| Index Entry | Section |
|---|
|
| S | | |
|---|
| Salcianu | 2.3.1 Purity |
| Salcianu | Acknowledgments |
| Sather | 1.3 Goals |
| Sather-K | 1.3 Goals |
| satisfaction, see correct implementation | 2.1.3.4 Correct Implementation |
| Saxe | Acknowledgments |
| Scherbring | Acknowledgments |
| Schneider | 3.1 Extensions to Java Expressions for Predicates |
| Seagren | Acknowledgments |
| semantics of signals clauses | 2.2.1.5 Specifying Exceptional Behavior |
| set comprehension | 3.1 Extensions to Java Expressions for Predicates |
| Shilling | Acknowledgments |
| side effects, freedom from in assertions | 3.1 Extensions to Java Expressions for Predicates |
| side-effects | 1.3 Goals |
| signals | 2.2.1.5 Specifying Exceptional Behavior |
| signals | 2.2.1.5 Specifying Exceptional Behavior |
| signals | 2.2.2.4 Pitfalls in Specifying Exceptions |
| signals clause | 2.2.2.4 Pitfalls in Specifying Exceptions |
| signals clauses, detailed | 2.2.2.3 Multiple Specification Cases |
| signals, default for | A. Specification Case Defaults |
| signals_only, default for | A. Specification Case Defaults |
| simultaneous exceptions | 2.2.2.4 Pitfalls in Specifying Exceptions |
| `spec' filename suffix | 1.4.1 Type Checking Specifications |
| `spec-refined' filename suffix | 1.4.1 Type Checking Specifications |
| spec_bigint_math | 1.1 Behavioral Interface Specification |
| spec_protected | 2.1.4 Models and Lightweight Specifications |
| spec_protected, as a model field shorthand | 2.1.4 Models and Lightweight Specifications |
| spec_public | 2.1.4 Models and Lightweight Specifications |
| spec_public, as a model field shorthand | 2.1.4 Models and Lightweight Specifications |
| specification case, nested | 2.3.2.2 JMLType and Informal Predicates |
| specification cases | 2.5.2 ArcType |
| specification cases, multiple | 2.2.2.3 Multiple Specification Cases |
| specification of examples | 2.3.2.1 Redundant Examples |
| specification of exceptions | 2.2.1.5 Specifying Exceptional Behavior |
| specification of exceptions | 2.2.2.4 Pitfalls in Specifying Exceptions |
| specification, completely omitted | A. Specification Case Defaults |
| specification, of methods | 2.2.1.3 Details of the Method Specifications |
| specification, of overriding method | 2.3.2.2 JMLType and Informal Predicates |
| specification, of subtypes | 2.6 Behavioral Subtyping |
| specification-only declaration | 1.3 Goals |
| Spivey | 1.3 Goals |
| Stata | Acknowledgments |
| static, history constraint | 2.2.1.2 Invariants and History Constraint |
| static, invariant | 2.2.1.2 Invariants and History Constraint |
| store-references, additions to Java for | 3.2 Extensions to Java Expressions for Store-Refs |
| subtype | 2.2.1.2 Invariants and History Constraint |
| subtype | 2.6 Behavioral Subtyping |
| subtype relation | 3.1 Extensions to Java Expressions for Predicates |
| subtype, adding to supertype's model | 2.6 Behavioral Subtyping |
| subtype, specification | 2.6 Behavioral Subtyping |
| subtyping, behavioral | 2.6 Behavioral Subtyping |
| suffixes, of filenames | 1.4.1 Type Checking Specifications |
| summation, see \sum | 3.1 Extensions to Java Expressions for Predicates |
| super, prohibited in assertions | 3.1 Extensions to Java Expressions for Predicates |
| supertype | 2.6 Behavioral Subtyping |
| supertype, specification of | 2.2.1.2 Invariants and History Constraint |
|
| T | | |
|---|
| Talpin | 3.1 Extensions to Java Expressions for Predicates |
| Tan | 1.1 Behavioral Interface Specification |
| Tan | 2.2.2.2 Redundant Specification |
| Tan | Acknowledgments |
| Tan | Acknowledgments |
| temporary side effects | 2.1.3.1 The Assignable Clause |
| termination function, for methods | 2.5.3 Digraph |
| termination, normal | 2.1.3.4 Correct Implementation |
| termination, of pure methods | 2.3.1 Purity |
| test data | 1.4.4 Unit Testing with JML |
| test oracle | 1.4.4 Unit Testing with JML |
| textual copying, and inheritance | 2.6 Behavioral Subtyping |
| Thomas | Acknowledgments |
| tool support, for JML | 1.4 Tool Support |
| type checking, of specifications | 1.4.1 Type Checking Specifications |
| type, correctness of implementation | 2.3.4 MoneyAC |
| typeof operator | 3.1 Extensions to Java Expressions for Predicates |
| types for mathematical modeling | 2.3 Types For Modeling |
| types, comparing | 3.1 Extensions to Java Expressions for Predicates |
| types, marking in expressions | 3.1 Extensions to Java Expressions for Predicates |
|
| U | | |
|---|
| undefinedness, in expressions | 3.1 Extensions to Java Expressions for Predicates |
| undefinedness, protection from | 2.2.1.5 Specifying Exceptional Behavior |
| undefinedness, protection from | 2.3.3 MoneyComparable and MoneyOps |
| unit testing, with JML | 1.4.4 Unit Testing with JML |
| universal quantifier, see \forall | 3.1 Extensions to Java Expressions for Predicates |
| University of Iowa, 22C:181 | Acknowledgments |
| University of Nijmegen | 1.3 Goals |
| University of Nijmegen | 1.4 Tool Support |
| URL, for JML | 4. Conclusions |
| URL, for JML | 4. Conclusions |
|
| V | | |
|---|
| value, vs. object model types | 2.3 Types For Modeling |
| van den Berg | Acknowledgments |
| van Dooren | Acknowledgments |
| VDM-SL | 1.3 Goals |
| Vermillard | Acknowledgments |
| Vickers | 1.3 Goals |
| Vickers | 1.3 Goals |
| Vickers | 2.1.1 Model Fields |
| visibility, and inheritance | 2.6 Behavioral Subtyping |
| von Henke | 1.1 Behavioral Interface Specification |
| von Wright | 1.3 Goals |
| von Wright | 1.3 Goals |
| von Wright | 2.1.1 Model Fields |
| von Wright | 2.3.6 USMoney |
|
| W | | |
|---|
| Wahls | 1.3 Goals |
| Wahls | Acknowledgments |
| web page, for JML | 4. Conclusions |
| web page, for JML | 4. Conclusions |
| Weck | 1.3 Goals |
| Weck | Acknowledgments |
| when, default for | A. Specification Case Defaults |
| Whitehead | 3.1 Extensions to Java Expressions for Predicates |
| Wills | 2.2.2.3 Multiple Specification Cases |
| Wing | 1. Introduction |
| Wing | 1.1 Behavioral Interface Specification |
| Wing | 1.3 Goals |
| Wing | 1.3 Goals |
| Wing | 2.1.1 Model Fields |
| Wing | 2.2.1.2 Invariants and History Constraint |
| Wing | 2.2.1.5 Specifying Exceptional Behavior |
| Wing | 2.2.2.3 Multiple Specification Cases |
| Wing | 2.3.3 MoneyComparable and MoneyOps |
| Wing | 2.4 Use of Pure Classes |
| Woodcock | 1.3 Goals |
| working_space, default for | A. Specification Case Defaults |
| Wright | 3.1 Extensions to Java Expressions for Predicates |
|