Java and the Java Virtual Machine

Introduction......Page 9
The goals of the book......Page 10
The contents of the book......Page 11
Decomposing Java and the JVM......Page 15
Sources and literature......Page 19
ASMs in a nutshell......Page 23
Mathematical definition of ASMs......Page 26
Notational conventions......Page 35
Part I. Java......Page 37
Static semantics of JavaI......Page 41
Transition rules for JavaI......Page 47
Static semantics of JavaC......Page 55
Transition rules for JavaC......Page 71
Static semantics of JavaO......Page 79
Transition rules for JavaO......Page 88
Static semantics of JavaE......Page 95
Transition rules for JavaE......Page 97
The concurrent extension JavaT of JavaE......Page 103
Static semantics of JavaT......Page 104
Transition rules for JavaT......Page 106
Thread invariants......Page 114
Structural properties of Java runs......Page 119
Unreachable statements......Page 125
Rules of definite assignment......Page 129
Java is type safe......Page 134
Part II. Compilation of Java: The Trustful JVM......Page 143
Dynamic semantics of the JVMI......Page 147
Compilation of JavaI......Page 150
Dynamic semantics of the JVMC......Page 155
Compilation of JavaC......Page 161
Dynamic semantics of the JVMO......Page 163
Compilation of JavaO......Page 165
Dynamic semantics of the JVME......Page 167
Compilation of JavaE......Page 171
Executing the JVMN......Page 173
The correctness statement......Page 175
The correctness proof......Page 186
Part III. Bytecode Verification: The Secure JVM......Page 213
The defensive virtual machine......Page 217
Checking JVMI......Page 218
Checking JVMC......Page 221
Checking JVMO......Page 222
Checking JVME......Page 227
Checking JVMN......Page 229
Checks are monotonic......Page 230
Bytecode type assignments......Page 231
Problems of bytecode verification......Page 232
Successors of bytecode instructions......Page 239
Type assignments without subroutine call stacks......Page 244
Soundness of bytecode type assignments......Page 250
Certifying compilation......Page 260
Principal bytecode type assignments......Page 281
Verifying JVMI......Page 283
Verifying JVMC......Page 287
Verifying JVME......Page 291
Verifying JVMN......Page 294
Initiating and defining loaders......Page 297
Loading classes......Page 298
Dynamic semantics of the JVMD......Page 299
Overview......Page 313
Java......Page 314
Compiler......Page 320
Java Virtual Machine......Page 322
Rules......Page 331
Arrays......Page 339
Trustful execution......Page 343
Defensive execution......Page 351
Diligent execution......Page 352
Check functions......Page 355
Successor functions......Page 356
Constraints......Page 357
Arrays......Page 359
Abstract versus real instructions......Page 363
Compilation functions......Page 369
maxOpd......Page 371
Arrays......Page 372
References......Page 373
List of Figures......Page 375
List of Tables......Page 379
Index......Page 381