Design by Contract, by Example Book

	Foreword	ix
	Preface	xi
Chapter 1	A First Taste of Design by Contract	1
1.1	About This Chapter	1
1.2	The Customer Manager Example	2
1.3	Some Questions	5
1.4	A Contract for CUSTOMER_MANAGER	6
1.5	The Story So Far	9
1.6	Runtime Checking	11
1.7	Trustworthy Documentation	13
1.8	Summary	15
1.9	An Aide Memoire	15
1.10	Things to Do	15
Chapter 2	Elementary Principles of Design by Contract	17
2.1	About This Chapter	17
2.2	Stacks	18
2.3	Separate Commands and Queries	19
2.4	Naming Conventions	22
2.5	Separate Basic Queries and Derived Queries	23
2.6	Specify How Commands Affect Basic Queries	26
2.7	Capture Unchanging Properties in Invariants	34
2.8	The Class and Its Contract	36
2.9	The Basic Queries Are a Conceptual Model of Stacks	38
2.10	The Six Principles	42
2.11	Things to Do	43
Chapter 3	Applying the Six Principles	47
3.1	About This Chapter	47
3.2	Dictionaries	47
3.3	Separating and Categorizing Features	48
3.4	Postconditions	50
3.5	Preconditions	56
3.6	Invariant	62
3.7	A Complete, Contract-Level View of DICTIONARY	63
3.8	Summary	65
3.9	Things to Do	66
Chapter 4	Building Support for Contracts--Immutable Lists	69
4.1	About This Chapter	69
4.2	Support for Linear Structures	69
4.3	Contracts Involve Expressions	70
4.4	Immutable Lists	71
4.5	A Contract for Immutable Lists	72
4.5.1	The Basic Queries	72
4.5.2	The Creation Command	74
4.5.3	The Derived Query count	74
4.5.4	The Derived Query preceded_by	74
4.5.5	The Derived Query item	75
4.5.6	The Derived Query is_equal	77
4.5.7	The Derived Query sublist	79
4.6	Summary	81
4.7	Things to Do	81
Chapter 5	Applying the Six Principles to QUEUE	83
5.1	About This Chapter	83
5.2	Queues	83
5.3	A Contract for the remove Feature	84
5.4	Making count a Derived Feature	88
5.5	A Contract for the Initialize Feature	91
5.6	A Contract for the head Feature	93
5.7	A Contract for the put Feature	94
5.8	More Derived Queries	94
5.9	Summary	95
5.10	Things to Do	96
Chapter 6	Design by Contract and Inheritance	99
6.1	About This Chapter	99
6.2	Superclasses and Subclasses	99
6.3	Redefining Contracts	100
6.3.1	Eiffel Syntax	104
6.3.2	Summary	107
6.4	Invariants and Inheritance	108
6.5	Designing Superclasses with Guarded Postconditions	109
6.6	Two Kinds of Inheritance	116
6.7	Summary	117
6.8	Things to Do	117
Chapter 7	Frame Rules	119
7.1	About This Chapter	119
7.2	Change Specifications and Frame Rules	119
7.3	Frame Rules for put Using Immutable Lists	121
7.4	Frame Rules for put Using "Forall"	128
7.5	Kinds of Frame Rules	130
7.6	Things to Do	132
7.7	Appendix: More About the Preprocessor	132
Chapter 8	Benefits of Design by Contract	137
8.1	About This Chapter	137
8.2	Kinds of Benefits	137
8.3	Better Designs	138
8.4	Improved Reliability	140
8.5	Better Documentation	140
8.6	Easier Debugging	142
8.7	Support for Reuse	142
8.8	Design by Contract and Defensive Programming	143
8.8.1	Defending a Program Against Unwanted Input	143
8.8.2	Bulletproofing a Routine	144
8.8.3	Defensive Programming	145
8.9	Some Costs and Limitations of Contracts	146
Chapter 9	Contracts for an Observer Framework	149
9.1	About This Chapter	149
9.2	The Observer Framework	150
9.3	Immutable Sets	152
9.4	Attaching and Detaching Observers	155
9.5	Notification (For One Observer)	156
9.6	Notification (For All Observers)	158
9.7	A Performance Issue	160
9.8	Frame Rules	161
9.9	Privacy	164
9.10	Things to Do	166
Chapter 10	Fulfilling a Precondition	169
10.1	About This Chapter	169
10.2	The Examples	170
10.3	Fulfilling and Testing a Precondition	170
10.4	Testing Versus Checking	172
10.5	A Simple Counter Class	173
10.6	The User's View of the Program	174
10.7	The Internal Structure of the Program	176
10.8	The Program's Behavior	178
10.9	A Minor Detail	184
10.10	Summary	186
10.11	Things to Do	187
Chapter 11	Java Examples	189
11.1	About This Chapter	189
11.2	Why Java?	190
11.3	Queues	190
11.3.1	The Basic Query size()	192
11.3.2	The Basic Query get()	193
11.3.3	The Derived Query head()	193
11.3.4	The Derived Query isEmpty()	194
11.3.5	The Derived Query shallowCopy()	194
11.3.6	The Constructor Queue	195
11.3.7	The Command put	196
11.3.8	The Command remove	196
11.3.9	Summary	198
11.4	Dictionaries	198
11.4.1	Names	199
11.4.2	The Invariant	200
11.4.3	The Basic Queries	200
11.4.4	A Derived Query	201
11.4.5	The Commands	201
11.4.6	The Constructor	202
11.4.7	A Possible Set of Classes	203
11.5	Java Without iContract	203
11.6	Precondition Testing	207
11.7	Things to Do	212
Chapter 12	Analysis by Contract	215
12.1	About This Chapter	215
12.2	A Use Case	215
12.3	Contracts in Analysis Models	217
12.4	A Contract for the withdrawCash Use Case	217
12.5	From Analysis to Design	220
12.6	Problem Domain and System Models	221
12.7	The Object Constraint Language	224
12.8	Summary	225
	Bibliography	227
	Index	231