Java Definite Assignment in Isabelle/HOL

Norbert Schirmer

Paper on the ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP'2003), July 21, 2003, Darmstadt, Germany


 Abstract

In Java the compiler guarantees that each local variable is initialised when we attempt to access it at runtime. This prohibits access to uninitialised memory during execution and is a key ingredient for type safety. We have formalised the definite assignment analysis of the Java compiler in the theorem prover Isabelle/HOL and proved it correct.

 Online Copy

Available as PDF-File (149KB)

 BibTeX Entry

@inproceedings{Schirmer-03-definite-assignment,
  author = 	 {Norbert Schirmer},
  title = 	 {{J}ava {D}efinite {A}ssignment in in {I}sabelle/{HOL}},
  booktitle = 	 {Formal Techniques for Java-like Programs 2003 (Proceedings)},
  year = 	 {2003},
  organization = {Chair of Software Engineering, ETH Zürich},
  editor = {Susan Eisenbach and Gary T. Leavens and Peter Müller and Arnd Poetzsch-Heffter and Erik Poll},
  note = 	 {Technical Report 108},
}


Norbert Schirmer
Last modified: Fri Jun 27 15:55:33 MEST 2003