[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

Concept Index: S -- W

Jump to:   !   (   *   +   -   .   /   ;   <   =   @   \   {   |  
A   B   C   D   E   F   G   H   I   J   K   L   M   N   O   P   Q   R   S   T   U   V   W   Z  

Index Entry Section

S
Salcianu2.3.1 Purity
SalcianuAcknowledgments
Sather1.3 Goals
Sather-K1.3 Goals
satisfaction, see correct implementation2.1.3.4 Correct Implementation
SaxeAcknowledgments
ScherbringAcknowledgments
Schneider3.1 Extensions to Java Expressions for Predicates
SeagrenAcknowledgments
semantics of signals clauses2.2.1.5 Specifying Exceptional Behavior
set comprehension3.1 Extensions to Java Expressions for Predicates
ShillingAcknowledgments
side effects, freedom from in assertions3.1 Extensions to Java Expressions for Predicates
side-effects1.3 Goals
signals2.2.1.5 Specifying Exceptional Behavior
signals2.2.1.5 Specifying Exceptional Behavior
signals2.2.2.4 Pitfalls in Specifying Exceptions
signals clause2.2.2.4 Pitfalls in Specifying Exceptions
signals clauses, detailed2.2.2.3 Multiple Specification Cases
signals, default forA. Specification Case Defaults
signals_only, default forA. Specification Case Defaults
simultaneous exceptions2.2.2.4 Pitfalls in Specifying Exceptions
`spec' filename suffix1.4.1 Type Checking Specifications
`spec-refined' filename suffix1.4.1 Type Checking Specifications
spec_bigint_math1.1 Behavioral Interface Specification
spec_protected2.1.4 Models and Lightweight Specifications
spec_protected, as a model field shorthand2.1.4 Models and Lightweight Specifications
spec_public2.1.4 Models and Lightweight Specifications
spec_public, as a model field shorthand2.1.4 Models and Lightweight Specifications
specification case, nested2.3.2.2 JMLType and Informal Predicates
specification cases2.5.2 ArcType
specification cases, multiple2.2.2.3 Multiple Specification Cases
specification of examples2.3.2.1 Redundant Examples
specification of exceptions2.2.1.5 Specifying Exceptional Behavior
specification of exceptions2.2.2.4 Pitfalls in Specifying Exceptions
specification, completely omittedA. Specification Case Defaults
specification, of methods2.2.1.3 Details of the Method Specifications
specification, of overriding method2.3.2.2 JMLType and Informal Predicates
specification, of subtypes2.6 Behavioral Subtyping
specification-only declaration1.3 Goals
Spivey1.3 Goals
StataAcknowledgments
static, history constraint2.2.1.2 Invariants and History Constraint
static, invariant2.2.1.2 Invariants and History Constraint
store-references, additions to Java for3.2 Extensions to Java Expressions for Store-Refs
subtype2.2.1.2 Invariants and History Constraint
subtype2.6 Behavioral Subtyping
subtype relation3.1 Extensions to Java Expressions for Predicates
subtype, adding to supertype's model2.6 Behavioral Subtyping
subtype, specification2.6 Behavioral Subtyping
subtyping, behavioral2.6 Behavioral Subtyping
suffixes, of filenames1.4.1 Type Checking Specifications
summation, see \sum3.1 Extensions to Java Expressions for Predicates
super, prohibited in assertions3.1 Extensions to Java Expressions for Predicates
supertype2.6 Behavioral Subtyping
supertype, specification of2.2.1.2 Invariants and History Constraint

T
Talpin3.1 Extensions to Java Expressions for Predicates
Tan1.1 Behavioral Interface Specification
Tan2.2.2.2 Redundant Specification
TanAcknowledgments
TanAcknowledgments
temporary side effects2.1.3.1 The Assignable Clause
termination function, for methods2.5.3 Digraph
termination, normal2.1.3.4 Correct Implementation
termination, of pure methods2.3.1 Purity
test data1.4.4 Unit Testing with JML
test oracle1.4.4 Unit Testing with JML
textual copying, and inheritance2.6 Behavioral Subtyping
ThomasAcknowledgments
tool support, for JML1.4 Tool Support
type checking, of specifications1.4.1 Type Checking Specifications
type, correctness of implementation2.3.4 MoneyAC
typeof operator3.1 Extensions to Java Expressions for Predicates
types for mathematical modeling2.3 Types For Modeling
types, comparing3.1 Extensions to Java Expressions for Predicates
types, marking in expressions3.1 Extensions to Java Expressions for Predicates

U
undefinedness, in expressions3.1 Extensions to Java Expressions for Predicates
undefinedness, protection from2.2.1.5 Specifying Exceptional Behavior
undefinedness, protection from2.3.3 MoneyComparable and MoneyOps
unit testing, with JML1.4.4 Unit Testing with JML
universal quantifier, see \forall3.1 Extensions to Java Expressions for Predicates
University of Iowa, 22C:181Acknowledgments
University of Nijmegen1.3 Goals
University of Nijmegen1.4 Tool Support
URL, for JML4. Conclusions
URL, for JML4. Conclusions

V
value, vs. object model types2.3 Types For Modeling
van den BergAcknowledgments
van DoorenAcknowledgments
VDM-SL1.3 Goals
VermillardAcknowledgments
Vickers1.3 Goals
Vickers1.3 Goals
Vickers2.1.1 Model Fields
visibility, and inheritance2.6 Behavioral Subtyping
von Henke1.1 Behavioral Interface Specification
von Wright1.3 Goals
von Wright1.3 Goals
von Wright2.1.1 Model Fields
von Wright2.3.6 USMoney

W
Wahls1.3 Goals
WahlsAcknowledgments
web page, for JML4. Conclusions
web page, for JML4. Conclusions
Weck1.3 Goals
WeckAcknowledgments
when, default forA. Specification Case Defaults
Whitehead3.1 Extensions to Java Expressions for Predicates
Wills2.2.2.3 Multiple Specification Cases
Wing1. Introduction
Wing1.1 Behavioral Interface Specification
Wing1.3 Goals
Wing1.3 Goals
Wing2.1.1 Model Fields
Wing2.2.1.2 Invariants and History Constraint
Wing2.2.1.5 Specifying Exceptional Behavior
Wing2.2.2.3 Multiple Specification Cases
Wing2.3.3 MoneyComparable and MoneyOps
Wing2.4 Use of Pure Classes
Woodcock1.3 Goals
working_space, default forA. Specification Case Defaults
Wright3.1 Extensions to Java Expressions for Predicates

Jump to:   !   (   *   +   -   .   /   ;   <   =   @   \   {   |  
A   B   C   D   E   F   G   H   I   J   K   L   M   N   O   P   Q   R   S   T   U   V   W   Z  


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Gary Leavens on March, 16 2009 using texi2html