Analysing the Java Package/Access Concepts in Isabelle/HOL

Norbert Schirmer


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

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

Norbert Schirmer
Last modified: Wed Dec 22 11:38:34 MET 2004