Preface xi
Acknowledgements xiii
Guide to the Reader xv
Codecharts xix
Propositions xxv
Prologue 1
1. Motivation 3
2. Design Description Languages 7
2.1 Theory Versus Practice 9
2.2 Decidability 11
2.3 Abstraction 12
2.4 Elegance 16
3. An Overview of Codecharts 19
3.1 Object-Orientation 19
3.2 Visualization 23
3.3 Rigour 26
3.4 Automated Verifiability 28
3.5 Scalability 30
3.6 Genericity 32
3.7 Minimality 33
3.8 Information Neglect 34
4.UML Versus Codecharts 37
5.Historical Notes 43
Part I: Practice 45
6. Modelling Small Programs 47
6.1 Modelling Individual Classes 49
6.2 Modelling Individual Methods 50
6.3 Modelling Properties 53
6.4 Modelling Implementation Minutia 55
6.5 Modelling Simple Relations 56
6.6 Modelling Indirect Relations 64
6.7 Subtyping 66
7. Modelling Large Programs 71
7.1 Modelling Sets of Classes 75
7.2 Modelling Total Relations Between Sets 77
7.3 Modelling Sets of Methods (Clans) 81
7.4 Modelling Isomorphic Relations 83
7.5 Modelling Sets of Methods (Tribes) 85
7.6 Modelling Class Hierarchies 90
7.7 Modelling Methods in Hierarchies 93
7.8 Modelling Properties of Sets 97
7.9 Case Study: Total Versus. Isomorphic 98
7.10 Case Study: JDOM 101
7.11 Case Study: Java 3D 103
8. Modelling Industry-Scale Programs 109
8.1 Modelling Sets of Hierarchies 111
8.2 Modelling Sets of Sets of Methods (Clans) 112
8.3 Modelling Sets of Sets of Methods (Tribes) 115
8.4 Modelling Total Relations Revisited 118
8.5 Modelling Isomorphic Relations Revisited 120
9. Modelling Design Motifs 127
10. Modelling Application Frameworks 133
10.1 Case Study: Enterprise JavaBeans 135
10.2 Case Study: JUnit 136
11. Modelling Design Patterns 139
11.1 Case Study: The Composite Pattern 140
11.2 Case Study: The Iterator Pattern 145
11.3 Case Study: The Factory Method Pattern 149
11.4 Case Study: The Abstract Factory Pattern 154
11.5 Concluding Remarks 157
12. Modelling Early Design Revisited 159
13. Advanced Modelling Techniques 161
13.1 Ad Hoc Symbols 161
13.2 Modelling Information Hiding 164
Part II: Theory 167
14. Abstract Semantics 169
14.1 Finite Structures 170
14.2 Abstract Semantics Functions 174
14.3 Design Models 174
14.4 Program Modelling Revisited 177
15. Verification 179
15.1 Verifying Closed Specifications 180
15.2 Verifying Open Specifications 183
15.3 Verifying Pattern Implementations 186
15.4 Tool Support for Automated Verification 188
16. Schemas 191
17. LePUS3 in Classical Logic 195
17.1 LePUS3 and Class-Z as First-Order Languages 195
17.2 Specifications in the Predicate Logic 196
17.3 The Axioms of Class-Based Programs 198
18. Reasoning about Charts 201
Appendix I: The Gang of Four Companion 213
Appendix II: Formal Definitions 229
Appendix III: UML Quick Reference 233
References 235
Index 239