Java and the Java Virtual Machine - Börger, Egon

. .

Résumé :
This book provides a high-level desription of Java and of the Java Virtual Machine....

Sommaire:
1. Introduction.- 1.1 The goals of the book.- 1.2 The contents of the book.- 1.3 Decomposing Java and the JVM.- 1.4 Sources and literature.- 2. Abstract State Machines.- 2.1 ASMs in a nutshell.- 2.2 Mathematical definition of ASMs.- 2.3 Notational conventions.- I. Java.- 3. The imperative core JavaI of Java.- 3.1 Static semantics of JavaI.- 3.2 Transition rules for JavaI.- 4. The procedural extension JavaC of JavaI.- 4.1 Static semantics of JavaC.- 4.2 Transition rules for JavaC.- 5. The object-oriented extension dollars dollars{\text{Jav}}{{\text{a}}_\mathcal{O}} dollars dollars of JavaC.- 5.1 Static semantics of dollars dollars{\text{Jav}}{{\text{a}}_\mathcal{O}} dollars dollars.- 5.2 Transition rules for dollars dollars{\text{Jav}}{{\text{a}}_\mathcal{O}} dollars dollars.- 6. The exception-handling extension Java? of dollars dollars{\text{Jav}}{{\text{a}}_\mathcal{O}} dollars dollars.- 6.1 Static semantics of Java?.- 6.2 Transition rules for Java?.- 7. The concurrent extension JavaT of Java?.- 7.1 Static semantics of JavaT.- 7.2 Transition rules for JavaT.- 7.3 Thread invariants.- 8. Java is type safe.- 8.1 Structural properties of Java runs.- 8.2 Unreachable statements.- 8.3 Rules of definite assignment.- 8.4 Java is type safe.- II. Compilation of Java: The Trustful JVM.- 9. The JVMI submachine.- 9.1 Dynamic semantics of the JVMI.- 9.2 Compilation of JavaI.- 10. The procedural extension JVMC of JVMI.- 10.1 Dynamic semantics of the JVMC.- 10.2 Compilation of JavaC.- 11. The object-oriented extension dollars dollars{\text{JV}}{{\text{M}}_\mathcal{O}} dollars dollars of JVMC.- 11.1 Dynamic semantics of the dollars dollars{\text{JV}}{{\text{M}}_\mathcal{O}} dollars dollars.- 11.2 Compilation of dollars dollars{\text{Jav}}{{\text{a}}_\mathcal{O}} dollars dollars.- 12. The exception-handling extension JVM? of dollars dollars{\text{JV}}{{\text{M}}_\mathcal{O}} dollars dollars.- 12.1 Dynamic semantics of the JVM?.- 12.2 Compilation of Java?.- 13. Executing the JVMN.- 14. Correctness of the compiler.- 14.1 The correctness statement.- 14.2 The correctness proof.- III. Bytecode Verification: The Secure JVM.- 15. The defensive virtual machine.- 15.1 Construction of the defensive JVM.- 15.2 Checking JVMI.- 15.3 Checking JVMC.- 15.4 Checking dollars dollars{\text{JV}}{{\text{M}}_\mathcal{O}} dollars dollars.- 15.5 Checking JVM?.- 15.6 Checking JVMN.- 15.7 Checks are monotonic.- 16. Bytecode type assignments.- 16.1 Problems of bytecode verification.- 16.2 Successors of bytecode instructions.- 16.3 Type assignments without subroutine call stacks.- 16.4 Soundness of bytecode type assignments.- 16.5 Certifying compilation.- 17. The diligent virtual machine.- 17.1 Principal bytecode type assignments.- 17.2 Verifying JVMI.- 17.3 Verifying JVMC.- 17.4 Verifying dollars dollars{\text{JV}}{{\text{M}}_\mathcal{O}} dollars dollars.- 17.5 Verifying JVM?.- 17.6 Verifying JVMN.- 18. The dynamic virtual machine.- 18.1 Initiating and defining loaders.- 18.2 Loading classes.- 18.3 Dynamic semantics of the JVMD.- A. Executable Models.- A.1 Overview.- A.2 Java.- A.3 Compiler.- A.4 Java Virtual Machine.- B. Java.- B.1 Rules.- B.2 Arrays.- C. JVM.- C.1 Trustful execution.- C.2 Defensive execution.- C.3 Diligent execution.- C.4 Check functions.- C.5 Successor functions.- C.6 Constraints.- C.7 Arrays.- C.8 Abstract versus real instructions.- D. Compiler.- D.1 Compilation functions.- D.2 maxOpd.- D.3 Arrays.- References.- List of Figures.- List of Tables.