| Index Entry | Section |
|---|
|
| S | | |
|---|
| Salcianu | 7.1.1.3 Pure Methods and Constructors |
| same field | 17.3 Type Checking Separate Files |
| same method | 17.3 Type Checking Separate Files |
| satisfaction of a package declaration | 5.1 Package Declarations |
| Saxe | 1.1 Behavioral Interface Specifications |
| Saxe | 2.4 Privacy Modifiers and Visibility |
| Saxe | 4.4 Annotation Markers |
| Saxe | 6.2.10 Monitored |
| Saxe | 6.2.11 Uninitialized |
| Saxe | 7.1.2.1 JML Modifiers for Fields |
| Saxe | G.1 Differences Between JML and Other Tools |
| Schneider | 2.7 Expression Evaluation and Undefinedness |
| semantics of non-helper method specifications | 9.6.2 Semantics of non-helper methods |
| semantics, of examples | 14.2 Redundant Examples |
| separating code and specification | 17.2 Using Separate Files |
| separating specification and code | 17.2 Using Separate Files |
| sequence vs. list, in grammar | 3. Syntax Notation |
| sequential behavior | 1.3 What is JML Good For? |
| set | 4.6 Tokens |
| set | 13.4.2 Set Statements |
| set comprehension | 12.5 Set Comprehensions |
| set-comprehension, defined | 12.5 Set Comprehensions |
| set-comprehension, used | 12.3 Expressions |
| set-statement, defined | 13.4.2 Set Statements |
| set-statement, used | 13.4 JML Annotation Statements |
| Shaner | 15.1 Ideas Behind Model Programs |
| shift-expr, defined | 12.3 Expressions |
| shift-expr, used | 12.3 Expressions |
| shift-op, defined | 12.3 Expressions |
| shift-op, used | 12.3 Expressions |
| short | 4.6 Tokens |
| short | 12.3 Expressions |
| sign, defined | 4.6 Tokens |
| sign, used | 4.6 Tokens |
| signals | 4.6 Tokens |
| signals | 9.6.2 Semantics of non-helper methods |
| signals | 9.6.2 Semantics of non-helper methods |
| signals | 9.9.4 Signals Clauses |
| signals clause, default for | 9.9.4 Signals Clauses |
| signals clause, omitted | 9.9.4 Signals Clauses |
| signals vs. signals_only | 9.8.1 Pragmatics of Exceptional Behavior Specifications Cases |
| signals-clause, defined | 9.9.4 Signals Clauses |
| signals-clause, used | Syntax |
| signals-clause, used | 15.6 Specification Statements |
| signals-keyword, defined | 9.9.4 Signals Clauses |
| signals-keyword, used | 9.9.4 Signals Clauses |
| signals-only-clause, defined | 9.9.5 Signals-Only Clauses |
| signals-only-clause, used | 15.6 Specification Statements |
| signals-only-clauses, multiple | 9.9.5 Signals-Only Clauses |
| signals-only-keyword, defined | 9.9.5 Signals-Only Clauses |
| signals-only-keyword, used | 9.9.5 Signals-Only Clauses |
| signals_only | 4.6 Tokens |
| signals_only | 9.6.2 Semantics of non-helper methods |
| signals_only | 9.6.2 Semantics of non-helper methods |
| signals_only | 9.8.1 Pragmatics of Exceptional Behavior Specifications Cases |
| signals_only | 9.9.5 Signals-Only Clauses |
| signals_only | 9.9.5 Signals-Only Clauses |
| signals_only, default for | 9.9.5 Signals-Only Clauses |
| signals_only, in comparing specifications | 14.1 Redundant Implications and Redundantly Clauses |
| signals_only_redundantly | 4.6 Tokens |
| signals_only_redundantly | 9.9.5 Signals-Only Clauses |
| signals_redundantly | 4.6 Tokens |
| signals_redundantly | 9.9.4 Signals Clauses |
| SignalsClause | 9.8.1 Pragmatics of Exceptional Behavior Specifications Cases |
| signed-integer, defined | 4.6 Tokens |
| signed-integer, used | 4.6 Tokens |
| simple-spec-body, defined | Syntax |
| simple-spec-body, used | Syntax |
| simple-spec-body, used | 14.2 Redundant Examples |
| simple-spec-body-clause, defined | Syntax |
| simple-spec-body-clause, used | Syntax |
| simple-spec-statement-body, defined | 15.6 Specification Statements |
| simple-spec-statement-body, used | 15.6 Specification Statements |
| simple-spec-statement-clause, defined | 15.6 Specification Statements |
| simple-spec-statement-clause, used | 15.6 Specification Statements |
| single line comment, see C++-Style comment | 4.3 Comments |
| single quote | 4.6 Tokens |
| single-character, defined | 4.6 Tokens |
| single-character, used | 4.6 Tokens |
| space | 4. Lexical Conventions |
| space, specification of | 12.4.12 \space |
| space, taken up by an object | 12.4.12 \space |
| space-expression, defined | 12.4.12 \space |
| space-expression, used | 12.4 JML Primary Expressions |
| spaces, defined | 4.2 Lexical Pragmas |
| spaces, used | 4.2 Lexical Pragmas |
| spec-array-initializer, defined | 12.4.24 Quantified Expressions |
| spec-array-initializer, used | 12.4.24 Quantified Expressions |
| spec-array-ref-expr, defined | 12.7 Store Refs |
| spec-array-ref-expr, used | 10.2 Dynamic Data Group Mappings |
| spec-array-ref-expr, used | 12.7 Store Refs |
| spec-case, defined | 9.2 Organization of Method Specifications |
| spec-case, used | 9.2 Organization of Method Specifications |
| spec-case-seq, defined | 9.2 Organization of Method Specifications |
| spec-case-seq, used | 9.2 Organization of Method Specifications |
| spec-case-seq, used | 14.1 Redundant Implications and Redundantly Clauses |
| spec-expression, defined | 12.2 Specification Expressions |
| spec-expression, used | 8.4 Represents Clauses |
| spec-expression, used | 9.9.12 Measured By Clauses |
| spec-expression, used | 9.9.14 Working Space Clauses |
| spec-expression, used | 9.9.15 Duration Clauses |
| spec-expression, used | 12.1 Predicates |
| spec-expression, used | 12.2 Specification Expressions |
| spec-expression, used | 12.4.2 \old and \pre |
| spec-expression, used | 12.4.10 \reach |
| spec-expression, used | 12.4.12 \space |
| spec-expression, used | 12.4.14 \nonnullelements |
| spec-expression, used | 12.4.16 \typeof |
| spec-expression, used | 12.4.17 \elemtype |
| spec-expression, used | 12.4.20 \max |
| spec-expression, used | 12.4.23 \lblneg and \lblpos |
| spec-expression, used | 12.4.24 Quantified Expressions |
| spec-expression, used | 12.7 Store Refs |
| spec-expression, used | 13.2.2 Loop Variant Functions |
| spec-expression, used | A.1.2 Deprecated Represents Clause Syntax |
| spec-expression-list, defined | 12.2 Specification Expressions |
| spec-expression-list, used | 8.9 Monitors For Clause |
| spec-expression-list, used | 12.4.9 \fresh |
| spec-expression-list, used | A.1.3 Deprecated Monitors For Clause Syntax |
| spec-header, defined | Syntax |
| spec-header, used | Syntax |
| spec-header, used | 14.2 Redundant Examples |
| spec-header, used | 15.6 Specification Statements |
| spec-initializer, defined | 12.4.24 Quantified Expressions |
| spec-initializer, used | 12.4.24 Quantified Expressions |
| spec-quantified-expr, defined | 12.4.24 Quantified Expressions |
| spec-quantified-expr, used | 12.4 JML Primary Expressions |
| spec-statement, defined | 15.6 Specification Statements |
| spec-statement, used | 13.4.3 Refining Statements |
| spec-statement, used | 15.3 Details of Model Programs |
| spec-var-decls, defined | 9.9.1 Specification Variable Declarations |
| spec-var-decls, used | Syntax |
| spec-var-decls, used | 14.2 Redundant Examples |
| spec-var-decls, used | 15.6 Specification Statements |
| spec-variable-declarator, defined | 12.4.24 Quantified Expressions |
| spec-variable-declarator, defined | 12.4.24 Quantified Expressions |
| spec-variable-declarator, used | 12.4.24 Quantified Expressions |
| spec-variable-declarators, defined | 12.4.24 Quantified Expressions |
| spec-variable-declarators, used | 9.9.1.2 Old Variable Declarations |
| spec_bigint_math | 4.6 Tokens |
| spec_bigint_math | 6.1.2 Modifiers for Type Declarations |
| spec_bigint_math | 6.2 Modifiers |
| spec_bigint_math | 6.2.12 Math Modifiers |
| spec_bigint_math | 6.2.12 Math Modifiers |
| spec_java_math | 4.6 Tokens |
| spec_java_math | 6.1.2 Modifiers for Type Declarations |
| spec_java_math | 6.2 Modifiers |
| spec_java_math | 6.2.12 Math Modifiers |
| spec_java_math | 6.2.12 Math Modifiers |
| spec_protected | 1.1 Behavioral Interface Specifications |
| spec_protected | 2.4 Privacy Modifiers and Visibility |
| spec_protected | 4.6 Tokens |
| spec_protected | 6.2 Modifiers |
| spec_protected | 6.2.4 Spec Protected |
| spec_protected, as a model field shorthand | 2.4 Privacy Modifiers and Visibility |
| spec_protected, modifier in separate file | 17.3 Type Checking Separate Files |
| spec_protected, modifier in separate file | 17.3 Type Checking Separate Files |
| spec_public | 1.1 Behavioral Interface Specifications |
| spec_public | 2.4 Privacy Modifiers and Visibility |
| spec_public | 4.6 Tokens |
| spec_public | 6.2 Modifiers |
| spec_public | 6.2.3 Spec Public |
| spec_public, as a model field shorthand | 2.4 Privacy Modifiers and Visibility |
| spec_public, modifier in separate file | 17.3 Type Checking Separate Files |
| spec_public, modifier in separate file | 17.3 Type Checking Separate Files |
| spec_safe_math | 4.6 Tokens |
| spec_safe_math | 6.1.2 Modifiers for Type Declarations |
| spec_safe_math | 6.2 Modifiers |
| spec_safe_math | 6.2.12 Math Modifiers |
| spec_safe_math | 6.2.12 Math Modifiers |
| special symbols | 4.6 Tokens |
| special-symbol, defined | 4.6 Tokens |
| special-symbol, used | 4. Lexical Conventions |
| specification for subtypes | 16. Specification for Subtypes |
| specification statement | 15.1 Ideas Behind Model Programs |
| specification, completely omitted | Semantics |
| specification, completeness of | 1.2 A First Example |
| specification, defined | 9.2 Organization of Method Specifications |
| specification, heavyweight | 2.3 Lightweight and Heavyweight Specifications |
| specification, in refining statement | 13.4.3 Refining Statements |
| specification, lightweight | 2.3 Lightweight and Heavyweight Specifications |
| specification, of interface behavior | 1.1 Behavioral Interface Specifications |
| specification, used | 9.2 Organization of Method Specifications |
| specification-only type | 6.1.2.2 Model Type Declarations |
| specifications for non-helper methods, semantics of | 9.6.2 Semantics of non-helper methods |
| specifications inheritance | 6.1.1 Subtyping for Type Declarations |
| specifications inheritance | 6.1.1 Subtyping for Type Declarations |
| specifications inheritance | 11. Specification Inheritance |
| specifying examples | 14.2 Redundant Examples |
| Spivey | 1.1 Behavioral Interface Specifications |
| Spivey | 1.5 Historical Precedents |
| stars-non-close, defined | 4.6 Tokens |
| stars-non-close, used | 4.6 Tokens |
| stars-non-slash, defined | 4.3 Comments |
| stars-non-slash, used | 4.3 Comments |
| start rule, in JML grammar | 5. Compilation Units |
| Stata | 1.6 Acknowledgments |
| Stata | G.1 Differences Between JML and Other Tools |
| state, post-state of a call | 9.6.2 Semantics of non-helper methods |
| state, pre-state of a call | 9.6.2 Semantics of non-helper methods |
| state, visible | 8.2 Invariants |
| statement, defined | 13. Statements and Annotation Statements |
| statement, refining | 13.4.3 Refining Statements |
| statement, used | 13. Statements and Annotation Statements |
| statement, used | 13.2 Loop Statements |
| statement, used | 13.4.3 Refining Statements |
| statement, used | 15.3 Details of Model Programs |
| static | 2.5 Instance vs. Static |
| static | 4.6 Tokens |
| static | 6.2 Modifiers |
| static | 7.2 Class Initializer Declarations |
| static | 8.2.1 Static vs. instance invariants |
| static | 8.3.1 Static vs. instance constraints |
| static constraint | 8.3.1 Static vs. instance constraints |
| static features | 2.5 Instance vs. Static |
| static invariant | 8.2 Invariants |
| static invariant | 8.2.1 Static vs. instance invariants |
| static invariant | 8.2.1 Static vs. instance invariants |
| static, modifier in separate file | 17.3 Type Checking Separate Files |
| static, modifier in separate file | 17.3 Type Checking Separate Files |
| static_initializer | 4.6 Tokens |
| static_initializer, separate files | 17.3 Type Checking Separate Files |
| static_initializer, used | 7.2 Class Initializer Declarations |
| status, of JML | 1.4 Status and Plans for JML |
| Steele | 4.6 Tokens |
| Steele | 4.6 Tokens |
| Steyaert | 16. Specification for Subtypes |
| store-ref, defined | 12.7 Store Refs |
| store-ref, used | 9.9.10 Accessible Clauses |
| store-ref, used | 9.9.10 Accessible Clauses |
| store-ref, used | 12.7 Store Refs |
| store-ref-expression, defined | 12.7 Store Refs |
| store-ref-expression, defined | 12.7 Store Refs |
| store-ref-expression, used | 8.4 Represents Clauses |
| store-ref-expression, used | 12.7 Store Refs |
| store-ref-expression, used | A.1.2 Deprecated Represents Clause Syntax |
| store-ref-keyword, defined | 12.7 Store Refs |
| store-ref-keyword, used | 9.9.11 Callable Clauses |
| store-ref-keyword, used | 12.7 Store Refs |
| store-ref-list, defined | 12.7 Store Refs |
| store-ref-list, used | 9.9.9 Assignable Clauses |
| store-ref-list, used | 9.9.10 Accessible Clauses |
| store-ref-list, used | 9.9.13 Captures Clauses |
| store-ref-list, used | 12.4.3 \not_assigned |
| store-ref-list, used | 12.4.4 \not_modified |
| store-ref-list, used | 12.4.5 \only_accessed |
| store-ref-list, used | 12.4.6 \only_assigned |
| store-ref-list, used | 12.4.8 \only_captured |
| store-ref-name, defined | 12.7 Store Refs |
| store-ref-name, used | 12.7 Store Refs |
| store-ref-name-suffix, defined | 12.7 Store Refs |
| store-ref-name-suffix, used | 12.7 Store Refs |
| strictfp | 4.6 Tokens |
| strictfp | 6.2 Modifiers |
| string-literal, defined | 4.6 Tokens |
| string-literal, used | 4.6 Tokens |
| string-literal, used | A.1.5 Deprecated Refine Prefix |
| strong validity | 2.7 Expression Evaluation and Undefinedness |
| subclass | 6.1.1 Subtyping for Type Declarations |
| subclassing_contract, replaced by code_contract | A.2 Replaced Syntax |
| subtype | 6.1.1 Subtyping for Type Declarations |
| subtype relation | 12.6.1 Subtype operator |
| subtype, for an interface | 6.1.1 Subtyping for Type Declarations |
| subtype, of an interface | 6.1.1 Subtyping for Type Declarations |
| subtypes, specification for | 16. Specification for Subtypes |
| subtyping | 6.1.1 Subtyping for Type Declarations |
| subtyping, for arrays, with ownership types | 18.6.1 Ownership Subtyping |
| subtyping, for ownership types | 18.6.1 Ownership Subtyping |
| suffixes, of filenames | 17.1 File Name Suffixes |
| SumArrayLoop | 13.2 Loop Statements |
| summation, see \sum | 12.4.24.2 Generalized Quantifiers |
| super | 4.6 Tokens |
| super | 8.3 Constraints |
| super | 10.1 Static Data Group Inclusions |
| super | 12.3 Expressions |
| super | 12.7 Store Refs |
| superclass | 6.1.1 Subtyping for Type Declarations |
| supertypes, specification of | 16. Specification for Subtypes |
| switch | 4.6 Tokens |
| switch | 13. Statements and Annotation Statements |
| switch-body, defined | 13. Statements and Annotation Statements |
| switch-body, used | 13. Statements and Annotation Statements |
| switch-label, defined | 13. Statements and Annotation Statements |
| switch-label, used | 13. Statements and Annotation Statements |
| switch-label-seq, defined | 13. Statements and Annotation Statements |
| switch-label-seq, used | 13. Statements and Annotation Statements |
| switch-statement, defined | 13. Statements and Annotation Statements |
| switch-statement, used | 13. Statements and Annotation Statements |
| synchronized | 4.6 Tokens |
| synchronized | 6.2 Modifiers |
| synchronized | 13. Statements and Annotation Statements |
| syntax notations | 3. Syntax Notation |
| syntax options | 4.6 Tokens |
| syntax, deprecated | A. Deprecated and Replaced Syntax |
| syntax, replaced | A. Deprecated and Replaced Syntax |
|