关键词: Java访问控制, 动态绑定, 形式分析, 定理证明

Abstract: Java access control is designed to provide security mechanisms on programming language level which prevent the users of an entity declared in a program from depending on unnecessary details of the implementation of this entity with different access modifiers. On the other hand, this design leads to the complexity of the semantics described in the Java language specification, and even the inconsistency between the specification and its implementation. After analyzing the Java access control mechanism which includes the accessibilities of class type, member invariables and member methods and the interactions between accessibility and inheritance, method overriding and dynamic binding, this paper gives strict definitions of these semantics in Isabelle/HOL 2015. Finally, this paper states and proves the properties that these definitions satisfy, which shows that this formalization is correct.

Key words: Java access control, dynamic binding, formal analysis, theorem proving