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}, }