| Index Entry | Section |
|---|
|
| V | | |
|---|
| validity, of assertions | 2.7 Expression Evaluation and Undefinedness |
| validity, strong | 2.7 Expression Evaluation and Undefinedness |
| value, abstract | 1.5 Historical Precedents |
| van den Berg | 1.6 Acknowledgments |
| variable-declarator, defined | 7.1.2 Field and Variable Declarations |
| variable-declarator, used | 7.1.2 Field and Variable Declarations |
| variable-declarators, defined | 7.1.2 Field and Variable Declarations |
| variable-declarators, used | 7.1.2 Field and Variable Declarations |
| variable-decls, defined | 7.1.2 Field and Variable Declarations |
| variable-decls, used | 7.1.2 Field and Variable Declarations |
| variable-decls, used | 13.1 Local Declaration Statements |
| variable-definition, defined | 7.1.2 Field and Variable Declarations |
| variable-definition, used | 7.1 Java Member Declarations |
| variant-function, defined | 13.2.2 Loop Variant Functions |
| variant-function, used | 13.2 Loop Statements |
| VDM | 1.5 Historical Precedents |
| VDM | 1.5 Historical Precedents |
| VDM-SL | 1.5 Historical Precedents |
| vertical tab | 4.1 White Space |
| Vickers | 1.5 Historical Precedents |
| virtual machine cycle time | 12.4.11 \duration |
| visibility | 1.3 What is JML Good For? |
| visibility | 2.4 Privacy Modifiers and Visibility |
| visibility, in JML | 2.4 Privacy Modifiers and Visibility |
| visibility, in lightweight specifications | 2.4 Privacy Modifiers and Visibility |
| visibility, in method specifications | 9.3 Access Control in Specification Cases |
| visible state | 8.2 Invariants |
| visible state, for a type | 8.2 Invariants |
| Vitek | 8.2 Invariants |
| Vitek | 18.1 Basic Concepts of Universes |
| vocabulary | 1.1 Behavioral Interface Specifications |
| void | 4.6 Tokens |
| void | 12.3 Expressions |
| void and pure methods | 7.1.1.3 Pure Methods and Constructors |
| volatile | 4.6 Tokens |
| volatile | 6.2 Modifiers |
| von Wright | 1.5 Historical Precedents |
| von Wright | 15. Model Programs |
|
| W | | |
|---|
| Watt | 4. Lexical Conventions |
| web site, for JML | 1. Introduction |
| Weck | 15.1 Ideas Behind Model Programs |
| when | 4.6 Tokens |
| when | 9.6.2 Semantics of non-helper methods |
| when | 9.6.2 Semantics of non-helper methods |
| when | 9.9.8 When Clauses |
| when clause, omitted | 9.9.8 When Clauses |
| when-clause, defined | 9.9.8 When Clauses |
| when-clause, used | Syntax |
| when-clause, used | 15.6 Specification Statements |
| when-keyword, defined | 9.9.8 When Clauses |
| when-keyword, used | 9.9.8 When Clauses |
| when_redundantly | 4.6 Tokens |
| when_redundantly | 9.9.8 When Clauses |
| while | 4.6 Tokens |
| while | 13.2 Loop Statements |
| while | 13.2 Loop Statements |
| white space | 4. Lexical Conventions |
| white space | 4.1 White Space |
| white-space | 5. Compilation Units |
| white-space, defined | 4.1 White Space |
| white-space, used | 4. Lexical Conventions |
| Wills | 1.1 Behavioral Interface Specifications |
| Wing | 1.1 Behavioral Interface Specifications |
| Wing | 1.5 Historical Precedents |
| Wing | 2.7 Expression Evaluation and Undefinedness |
| working space, specification of | 12.4.13 \working_space |
| working-space-clause, defined | 9.9.14 Working Space Clauses |
| working-space-clause, used | Syntax |
| working-space-clause, used | 15.6 Specification Statements |
| working-space-expression, defined | 12.4.13 \working_space |
| working-space-expression, used | 12.4 JML Primary Expressions |
| working-space-keyword, defined | 9.9.14 Working Space Clauses |
| working-space-keyword, used | 9.9.14 Working Space Clauses |
| working_space | 4.6 Tokens |
| working_space | 9.6.2 Semantics of non-helper methods |
| working_space | 9.6.2 Semantics of non-helper methods |
| working_space | 9.9.14 Working Space Clauses |
| working_space_redundantly | 4.6 Tokens |
| working_space_redundantly | 9.9.14 Working Space Clauses |
| writable | 4.6 Tokens |
| writable | 8.8 Writable If Clauses |
| writable-if-clause, defined | 8.8 Writable If Clauses |
| writable-if-clause, used | 8. Type Specifications |
|
| Z | | |
|---|
| Z | 1.1 Behavioral Interface Specifications |
| Z | 1.5 Historical Precedents |
| zero-to-three, defined | 4.6 Tokens |
| zero-to-three, used | 4.6 Tokens |
|