Premium
Analysing the Java package/access concepts in Isabelle/HOL
Author(s) -
Schirmer Norbert
Publication year - 2004
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.800
Subject(s) - hol , computer science , programming language , java , semantics (computer science) , proof assistant , theoretical computer science , mathematical proof , mathematics , geometry
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. Copyright © 2004 John Wiley & Sons, Ltd.