Analysing the Java Package/Access Concepts in Isabelle/HOL

Norbert Schirmer

Paper on the ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP'2002), June 10, 2002, Malaga, Spain


Java access modifiers and packages provide a mechanism to restrict the access to members and types as additional means of information hiding beyond the pure object oriented concept of classes. In this paper we clarify the semantics of access modifiers and packages by adding them to our formal model of Java in the theorem prover Isabelle/HOL. We analyse which properties we can rely on at runtime, provided that the static accessibility tests have been passed.

 Online Copy

Available as PDF-File (174KB)

 BibTeX Entry

  author = 	 {Norbert Schirmer},
  title = 	 {Analysing the {J}ava {P}ackage/{A}ccess {C}oncepts in {I}sabelle/{HOL}},
  booktitle = 	 {Formal Techniques for Java-like Programs 2003 (Proceedings)},
  year = 	 {2002},
  organization = {Computing Science Department, University of Nijmegen},
  editor = {Erik Poll},
  note = {Technical Report NIII-R0204},

Norbert Schirmer
Last modified: Wed Sep 25 15:32:45 MEST 2002