Java access modifiers and packages provide a mechanism to restrict access to members and types, as an additional means of information hiding beyond the purely 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 program has passed the static accessibility tests.

Online Copy

Preprint available as PDF-File (282KB)

BibTeX Entry

@article{Schirmer-04-access, author = {Norbert Schirmer}, title = {Analysing the {J}ava package/access concepts in {I}sabelle/{HOL}}, journal = {Concurrency and Computation: Practice and Experience}, volume = "16", number = "7", pages = "689-706", year = "2004", }