Skip to main content
SpringerLink
Log in

Java — formal fundiert*

  • Conference paper
JIT’98 Java-Informations-Tage 1998

Part of the book series: Informatik aktuell ((INFORMAT))

  • 788 Accesses

Zusammenfassung

Dieser Artikel gibt eine Übersicht über das Projekt Bali zur formalen Behandlung möglichst vieler Aspekte von Java. Die Arbeiten umfassen bisher eine formale Semantik großer Teile der JavaQuellsprache und des Bytecodes, jeweils zusammen mit einem Beweis der Typsicherheit. Als Spezifikations- und Verifikationswerkzeug dient Isabelle/HOL. Wir beschreiben die Ziele dieses Projekts und die grobe Vorgehensweise, geben einen knappen Einblick in die Formalisierung und die bewiesenen Aussagen, und stellen unsere bisherigen Ergebnisse und Erfahrungen dar.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literatur

  1. Ole Agesen, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language. In ACM Symp. Object-Oriented Programming: Systems, Languages and Applications, 1997.

    Google Scholar 

  2. Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Generic Java specification. Draft version, 1998.

    Google Scholar 

  3. Egon Börger and Wolfram Schulte. A mathematical definition of the dynamic semantics of Java. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer-Verlag, 1998.

    Google Scholar 

  4. Richard M. Cohen. The defensive Java Virtual Machine specification. Technical report, Computational Logic Inc., 1997. Draft version.

    Google Scholar 

  5. Sophia Drossopoulou and Susan Eisenbach. Towards an operational semantics and proof of type soundness for Java. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer-Verlag, 1998.

    Google Scholar 

  6. James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.

    Google Scholar 

  7. Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.

    Google Scholar 

  8. Tobias Nipkow, David von Oheimb, and Cornelia Pusch. Project Bali. 1998. http://www.in.tum.de/ isabelle/bali/.

  9. David von Oheimb and Tobias Nipkow. Machine-checking the Java specification: Proving type-safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer-Verlag, 1998.

    Google Scholar 

  10. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994.

    Google Scholar 

  11. Cornelia Pusch. Formalizing the Java Virtual Machine in Isabelle. Technical Report TUM-I9816, Institut für Informatik, Technische Universiät München, 1998.

    Google Scholar 

  12. Zhenyu Qian. A formal specification of Java Virtual Machine instructions. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer-Verlag, 1998.

    Google Scholar 

  13. Donald Syme. Proving Java type soundness. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer-Verlag, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität München, Germany

    David von Oheimb & Cornelia Pusch

Authors
  1. David von Oheimb
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cornelia Pusch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Lehrstuhl für Informations- und Kommunikationsdienste, Fachbereich Informatik, Universität Rostock, Albert-Einstein-Strasse 21, D-18059, Rostock, Germany

    Clemens H. Cap

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

von Oheimb, D., Pusch, C. (1999). Java — formal fundiert*. In: Cap, C.H. (eds) JIT’98 Java-Informations-Tage 1998. Informatik aktuell. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-59984-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-59984-2_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64971-7

  • Online ISBN: 978-3-642-59984-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation