计算机科学与探索 ›› 2016, Vol. 10 ›› Issue (11): 1501-1511.DOI: 10.3778/j.issn.1673-9418.1606039
江 南1,2+,何炎祥1,3,张晓瞳1,刘 瑞1,沈云飞1
JIANG Nan1,2+, HE Yanxiang1,3, ZHANG Xiaotong1, LIU RUI1, SHEN Yunfei1
摘要: Java访问控制一方面提供了语言级的安全性机制,这种机制针对程序中所声明的实体,通过不同的访问修饰符,向其使用者屏蔽实体的实现细节;另一方面,它也导致了该语言规范的复杂性和实现的不一致性。分析了Java访问控制机制,包括类型、成员变量和成员方法的可访问性,以及可访问性与继承关系、方法覆盖、动态绑定之间的交互;然后使用定理证明助手Isabelle/HOL 2015严格定义了这些语义规范;最后陈述并证明了这些定义所满足的性质定理,从而表明该形式化定义的正确性。