| Index Entry | Section |
|---|
|
| ! | | |
|---|
| !=, for booleans | 3.1 Extensions to Java Expressions for Predicates |
|
| ( | | |
|---|
| (* | 2.3.2.2 JMLType and Informal Predicates |
| (* | 3.1 Extensions to Java Expressions for Predicates |
|
| * | | |
|---|
| *) | 2.3.2.2 JMLType and Informal Predicates |
| *) | 3.1 Extensions to Java Expressions for Predicates |
| *, in array range | 3.2 Extensions to Java Expressions for Store-Refs |
|
| + | | |
|---|
| ++, prohibited in assertions | 3.1 Extensions to Java Expressions for Predicates |
| +=, prohibited in assertions | 3.1 Extensions to Java Expressions for Predicates |
|
| - | | |
|---|
| --, prohibited in assertions | 3.1 Extensions to Java Expressions for Predicates |
| -=, prohibited in assertions | 3.1 Extensions to Java Expressions for Predicates |
| -R option to jml script | 1.4.1 Type Checking Specifications |
|
| . | | |
|---|
| .. | 3.2 Extensions to Java Expressions for Store-Refs |
| `.java' | 1.4.1 Type Checking Specifications |
| .java files | 1.1 Behavioral Interface Specification |
| `.java-refined' | 1.4.1 Type Checking Specifications |
| `.jml' | 1.1 Behavioral Interface Specification |
| `.jml' | 1.4.1 Type Checking Specifications |
| `.jml-refined' | 1.1 Behavioral Interface Specification |
| `.jml-refined' | 1.4.1 Type Checking Specifications |
| .jml-refined files | 1.1 Behavioral Interface Specification |
| `.refines-java' | 1.4.1 Type Checking Specifications |
| `.refines-jml' | 1.4.1 Type Checking Specifications |
| `.refines-spec' | 1.4.1 Type Checking Specifications |
| `.spec' | 1.1 Behavioral Interface Specification |
| `.spec' | 1.4.1 Type Checking Specifications |
| `.spec-refined' | 1.1 Behavioral Interface Specification |
| `.spec-refined' | 1.4.1 Type Checking Specifications |
|
| / | | |
|---|
| /*+@ vs. /*@ annotations | 1.1 Behavioral Interface Specification |
| /*@ | 1.1 Behavioral Interface Specification |
| // | 1.1 Behavioral Interface Specification |
| //@ | 1.1 Behavioral Interface Specification |
|
| ; | | |
|---|
| ;, in quantifiers | 3.1 Extensions to Java Expressions for Predicates |
|
| < | | |
|---|
| <- | 2.6 Behavioral Subtyping |
| </esc> | 1.1 Behavioral Interface Specification |
| </jml> | 1.1 Behavioral Interface Specification |
| </pre></esc> | 1.1 Behavioral Interface Specification |
| </pre></jml> | 1.1 Behavioral Interface Specification |
| <: | 3.1 Extensions to Java Expressions for Predicates |
| <=!=> | 3.1 Extensions to Java Expressions for Predicates |
| <== | 3.1 Extensions to Java Expressions for Predicates |
| <==> | 2.2.1.3 Details of the Method Specifications |
| <==> | 3.1 Extensions to Java Expressions for Predicates |
| <esc> | 1.1 Behavioral Interface Specification |
| <jml> | 1.1 Behavioral Interface Specification |
| <pre><esc> | 1.1 Behavioral Interface Specification |
| <pre><jml> | 1.1 Behavioral Interface Specification |
|
| = | | |
|---|
| =, prohibited in assertions | 3.1 Extensions to Java Expressions for Predicates |
| ==, for booleans | 3.1 Extensions to Java Expressions for Predicates |
| ==, to compare values | 2.2.1.3 Details of the Method Specifications |
| ==, vs equals | 2.1.3.3 Reference Semantics |
| ==, vs. equals | 2.1.3.3 Reference Semantics |
| ==> | 3.1 Extensions to Java Expressions for Predicates |
|
| @ | | |
|---|
| @*/ | 1.1 Behavioral Interface Specification |
| @, in annotations | 2.2.1.3 Details of the Method Specifications |
|
| \ | | |
|---|
| \elemtype | 3.1 Extensions to Java Expressions for Predicates |
| \exists | 3.1 Extensions to Java Expressions for Predicates |
| \forall | 3.1 Extensions to Java Expressions for Predicates |
| \fresh | 3.1 Extensions to Java Expressions for Predicates |
| \into | 2.2.2.1 Data Groups and Represents Clauses |
| \max | 3.1 Extensions to Java Expressions for Predicates |
| \min | 3.1 Extensions to Java Expressions for Predicates |
| \nonnullelements | 3.1 Extensions to Java Expressions for Predicates |
| \not_specified | A. Specification Case Defaults |
| \not_specified | A. Specification Case Defaults |
| \nothing | 2.1.3.1 The Assignable Clause |
| \num_of | 3.1 Extensions to Java Expressions for Predicates |
| \old | 1.3 Goals |
| \old | 2.1.3.2 Old Values |
| \old | 3.1 Extensions to Java Expressions for Predicates |
| \old, pitfalls of | 2.1.3.2 Old Values |
| \old, semantics of | 2.1.3.2 Old Values |
| \product | 3.1 Extensions to Java Expressions for Predicates |
| \result | 1.1 Behavioral Interface Specification |
| \result | 3.1 Extensions to Java Expressions for Predicates |
| \such_that | 2.6 Behavioral Subtyping |
| \sum | 3.1 Extensions to Java Expressions for Predicates |
| \type | 3.1 Extensions to Java Expressions for Predicates |
| \typeof | 3.1 Extensions to Java Expressions for Predicates |
|
| { | | |
|---|
| {| | 2.3.2.2 JMLType and Informal Predicates |
| {| | 2.5.3 Digraph |
| {|} | 3.1 Extensions to Java Expressions for Predicates |
|
| | | | |
|---|
| |} | 2.3.2.2 JMLType and Informal Predicates |
| |} | 2.5.3 Digraph |
|
| A | | |
|---|
| abstract data type, implementation of | 2.2.2.1 Data Groups and Represents Clauses |
| abstract data types | 2.1 Abstract Models |
| abstract model | 2.2.1 Specification of BoundedThing |
| abstract model, adding to | 2.2.2 Specification of BoundedStackInterface |
| abstract modeling classes | 2.3 Types For Modeling |
| abstract models | 2.1 Abstract Models |
| abstraction function, see represents clause | 2.2.2.1 Data Groups and Represents Clauses |
| abstraction relation, see represents clause | 2.2.2.1 Data Groups and Represents Clauses |
| abstraction relations | 2.6 Behavioral Subtyping |
| acknowledgments | Acknowledgments |
| adding, to abstract model | 2.2.2 Specification of BoundedStackInterface |
| adding, to method specification | 2.2.1.4 Adding to Method Specifications |
| adding, to supertype's model | 2.6 Behavioral Subtyping |
| addition, quantified see \sum | 3.1 Extensions to Java Expressions for Predicates |
| ADT, correctness of implementation | 2.3.4 MoneyAC |
| ADT, implementation of | 2.2.2.1 Data Groups and Represents Clauses |
| ADT, modeling | 2.5 Composition for Container Classes |
| ADT, specification of | 2.1 Abstract Models |
| allocation, vs. modification | 2.1.3.1 The Assignable Clause |
| also | 2.2.1.4 Adding to Method Specifications |
| also | 2.2.2.3 Multiple Specification Cases |
| also | 2.2.2.3 Multiple Specification Cases |
| also | 2.3.2.2 JMLType and Informal Predicates |
| also | 2.3.2.2 JMLType and Informal Predicates |
| also | 2.5.2 ArcType |
| also | 2.6 Behavioral Subtyping |
| Amtoft | 3.1 Extensions to Java Expressions for Predicates |
| annotation markers | 1.1 Behavioral Interface Specification |
| annotations | 1.1 Behavioral Interface Specification |
| annotations | 1.1 Behavioral Interface Specification |
| annotations, in documentation comments | 1.1 Behavioral Interface Specification |
| annotations, placement of | 1.1 Behavioral Interface Specification |
| Arnold | 1. Introduction |
| array range | 3.2 Extensions to Java Expressions for Store-Refs |
| array ranges | 3.2 Extensions to Java Expressions for Store-Refs |
| array, specifying elements are non-null | 3.1 Extensions to Java Expressions for Predicates |
| assert | 2.3.5 MoneyComparableAC |
| assertion checking | 1.4.3 Run Time Assertion Checking |
| assertion, embedded | 2.3.5 MoneyComparableAC |
| assertions, additions to Java expressions for | 3.1 Extensions to Java Expressions for Predicates |
| assertions, expressions in | 1.1 Behavioral Interface Specification |
| assertions, in Java vs. JML | 2.3.5 MoneyComparableAC |
| assertions, Java expressions prohibited in | 3.1 Extensions to Java Expressions for Predicates |
| assertions, semantics of | 3.1 Extensions to Java Expressions for Predicates |
| assign to, locations a method can | 2.1.3.1 The Assignable Clause |
| assignable | 2.1.3.1 The Assignable Clause |
| assignable | 2.1.3.1 The Assignable Clause |
| assignable | 2.1.3.4 Correct Implementation |
| assignable | 2.2 Data Groups |
| assignable | 2.2.2.1 Data Groups and Represents Clauses |
| assignable | 2.3.6 USMoney |
| assignable clause | 2.1.3.1 The Assignable Clause |
| assignable clause | 3.2 Extensions to Java Expressions for Store-Refs |
| assignable clause | 3.2 Extensions to Java Expressions for Store-Refs |
| assignable clause, and constructors | 2.3.6 USMoney |
| assignable clause, and data groups | 2.2.2.1 Data Groups and Represents Clauses |
| assignable clause, checks | 2.1.3.1 The Assignable Clause |
| assignable clause, redundancy in | 2.3.6 USMoney |
| assignable clause, semantics of | 2.1.3.1 The Assignable Clause |
| assignable clauses, and data groups | 2.2.2.1 Data Groups and Represents Clauses |
| assignable, default for | A. Specification Case Defaults |
| assignable_redundantly | 2.3.6 USMoney |
| assignment | 3.1 Extensions to Java Expressions for Predicates |
| assignment, to model variables | 2.1.3.1 The Assignable Clause |
| assume | 2.3.6 USMoney |
|