Buch, Englisch, 381 Seiten, Book w. online files/update, Format (B × H): 165 mm x 244 mm, Gewicht: 725 g
Definition, Verification, Validation
Buch, Englisch, 381 Seiten, Book w. online files/update, Format (B × H): 165 mm x 244 mm, Gewicht: 725 g
ISBN: 978-3-540-42088-0
Verlag: Springer-Verlag GmbH
Zielgruppe
Research
Autoren/Hrsg.
Fachgebiete
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Compiler
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmierung: Methoden und Allgemeines
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Webprogrammierung
- Mathematik | Informatik EDV | Informatik Betriebssysteme Windows Betriebssysteme
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Prozedurale Programmierung
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Software Engineering Objektorientierte Softwareentwicklung
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmier- und Skriptsprachen
Weitere Infos & Material
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 $${\text{Jav}}{{\text{a}}_\mathcal{O}}$$ of JavaC.- 5.1 Static semantics of $${\text{Jav}}{{\text{a}}_\mathcal{O}}$$.- 5.2 Transition rules for $${\text{Jav}}{{\text{a}}_\mathcal{O}}$$.- 6. The exception-handling extension Java? of $${\text{Jav}}{{\text{a}}_\mathcal{O}}$$.- 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 $${\text{JV}}{{\text{M}}_\mathcal{O}}$$ of JVMC.- 11.1 Dynamic semantics of the $${\text{JV}}{{\text{M}}_\mathcal{O}}$$.- 11.2 Compilation of $${\text{Jav}}{{\text{a}}_\mathcal{O}}$$.- 12. The exception-handling extension JVM? of $${\text{JV}}{{\text{M}}_\mathcal{O}}$$.- 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 $${\text{JV}}{{\text{M}}_\mathcal{O}}$$.- 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 $${\text{JV}}{{\text{M}}_\mathcal{O}}$$.- 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.