Object-Oriented Technology

The core idea of this book is that objectℓ́ℓ oriented technology is a generic technology whose various technical aspects can be presented in a unified and consistent framework. This applies to both practical and formal aspects of object-oriented technology. Course tested in a variety of object-oriented courses, numerous examples, figures and exercises are presented in each chapter. The approach in this book is based on typed technologies, and the core notions fit mainstream object-oriented languages such as Java and C♯. The book promotes object-oriented constraints (assertions), their specification and verification. Object-oriented constraints apply to specification and verification of object-oriented programs, specification of the object-oriented platform, more advanced concurrent models, database integrity constraints and object-oriented transactions, their specification and verification Preface 8 Acknowledgements 10 Contents 12 1 Typed Objects 16 1.1 Typed Objects 16 1.1.1 Objects and Classes 16 1.1.2 Inheritance 18 1.1.3 Subtyping 21 1.1.4 Static and Dynamic Binding 24 1.2 Parametric Types 27 1.2.1 Collection Types 27 1.2.2 Parametric Types 30 1.2.3 Implementing Parametric Classes 32 1.2.4 Abstract Classes 32 1.2.5 Parametric Types and Subtyping 35 1.3 Bibliographic Remarks 36 1.4 Exercises 36 References 38 2 Assertions 39 2.1 Declarative Specifications 39 2.1.1 Assertions 39 2.1.2 Basic Reasoning Rules 41 2.2 Object-Oriented Assertions 45 2.2.1 Preconditions and Postconditions 46 2.2.2 Loop Invariants 47 2.2.3 Termination 48 2.2.4 Object Invariants 49 2.2.5 Assertions for Collections 51 2.2.6 Behavioral Subtyping 54 2.3 Sample Application 56 2.4 Bibliographic Remarks 60 2.5 Exercises 61 References 62 3 Virtual Platform 63 3.1 Reflection 64 3.1.1 Reflective Classes 64 3.1.2 Class Objects 65 3.1.3 Field Objects 67 3.1.4 Method Objects 68 3.1.5 Constructor Objects 68 3.1.6 Updating Fields 69 3.1.7 Invoking Methods 69 3.1.8 Creating Class Objects 70 3.1.9 Class Files 71 3.2 Virtual Machine 72 3.2.1 The Structure of the Virtual Machine 72 3.2.2 Creating Objects 74 3.2.3 Invoking Methods 75 3.2.4 Accessing Fields 75 3.2.5 Operations 77 3.2.6 Arrays 78 3.3 Extending Virtual Platform 81 3.4 Persistent Objects 85 3.4.1 Orthogonal Persistence 85 3.4.2 Persistence Architecture 88 3.4.3 Object Serialization 89 3.5 Bibliographic Remarks 91 3.6 Exercises 92 References 93 4 Type Systems 94 4.1 Formal Type Systems 95 4.1.1 Typing Rules 95 4.1.2 Object-Oriented Type System 97 4.1.3 Dynamic Type Checking 101 4.1.4 Parametric Types 102 4.2 Reflection 104 4.3 Type Erasure 107 4.3.1 Type Erasure Idiom 107 4.3.2 Static Type Checking 108 4.3.3 Dynamic Type Checking 112 4.3.4 Persistence by Serializability 112 4.3.5 Reflection 114 4.4 Bibliographic Remarks 115 4.5 Exercises 115 References 116 5 Concurrent Models 118 5.1 Concurrent Threads 118 5.1.1 Thread Objects 118 5.1.2 Synchronized Objects 120 5.1.3 Synchronization and Inheritance 122 5.1.4 Concurrency and Serialization 123 5.1.5 Synchronized Versus Unsynchronized Executions 124 5.2 Messages as Objects 126 5.2.1 Types of Messages 126 5.2.2 Typing Rules 129 5.2.3 Behavioral Subtyping 132 5.3 Concurrent Objects 133 5.3.1 Ambients of Concurrent Objects 133 5.3.2 Reflection 137 5.3.3 Virtual Machine 140 5.4 Bibliographic Remarks 143 5.5 Exercises 143 References 144 6 Object Databases 146 6.1 Query Languages 147 6.1.1 Object Definition Language 147 6.1.2 Object Query Language 148 6.1.3 Java OQL 150 6.1.4 Language Integrated Queries (LINQ) 154 6.2 Object Databases 157 6.2.1 ODMG Java Binding 157 6.2.2 Parametric Persistent Collections 162 6.2.3 Db4 Objects 164 6.2.4 Database Application 168 6.3 Database Constraints 171 6.4 Bibliographic Remarks 175 6.5 Exercises 176 References 177 7 Types and Constraints 178 7.1 Database Type Systems 179 7.1.1 ODL and OQL Examples 179 7.1.2 Schemas 180 7.1.3 Inheritance 181 7.1.4 Structures 182 7.1.5 Interfaces 183 7.1.6 Classes 185 7.1.7 Objects and Messages 186 7.1.8 Type Checking OQL Queries 187 7.1.9 OQL Queries and Parametric Types 191 7.1.10 Queries with Order by Clause 192 7.1.11 Java OQL 194 7.1.12 Typing Ordered Collections and Indices 197 7.2 Transactions 199 7.2.1 Transactions and Constraints 199 7.2.2 Schemas and Transactions 201 7.2.3 Levels of Consistency 202 7.2.4 Constraints for Schemas 204 7.2.5 Sample Transactions 205 7.2.6 Constraints and Queries 207 7.2.7 Specification Inheritance 208 7.2.8 Abstraction 211 7.2.9 Dynamic Checking of Constraints 212 7.3 Bibliographic Remarks 213 7.4 Exercises 213 References 214 Index 216 The core idea of this book is that objectĺl oriented technology is a generic technology whose various technical aspects can be presented in a unified and consistent framework. This applies to both practical and formal aspects of object-oriented technology. Course tested in a variety of object-oriented courses, numerous examples, figures and exercises are presented in each chapter. The approach in this book is based on typed technologies, and the core notions fit mainstream object-oriented languages such as Java and C♯. The book promotes object-oriented constraints (assertions), their specification and verification. Object-oriented constraints apply to specification and verification of object-oriented programs, specification of the object-oriented platform, more advanced concurrent models, database integrity constraints and object-oriented transactions, their specification and verification Front Matter....Pages i-xiv Typed Objects....Pages 1-23 Assertions....Pages 25-48 Virtual Platform....Pages 49-79 Type Systems....Pages 81-104 Concurrent Models....Pages 105-132 Object Databases....Pages 133-164 Types and Constraints....Pages 165-202 Back Matter....Pages 203-209