基于JML的标记—清扫垃圾收集验证  

MARK-AND-SWEEP GARBAGE COLLECTION VERIFICATION BASED ON JML

作　　者：宋玉婷[1] 孙文辉[1] 

机构地区：[1]北京交通大学计算机与信息技术学院,北京100044

出　　处：《计算机应用与软件》2014年第9期32-36,共5页Computer Applications and Software

摘　　要：Java中的垃圾收集机制,有效地避免了安全漏洞也提高了资源利用率。然而对于和用户程序并行执行的垃圾收集,其过程及算法的实现甚是复杂,使得可靠性难以保证。目前,基于契约的程序动态分析技术已成为软件质量保证的一个重要途径。而JML继承了契约式设计的所有优点,成为一种为Java量身定做的形式化的行为接口规范语言,用来规范Java程序模块的行为及详细设计决策。基于这种思想,通过前置条件、后置条件等规范对垃圾收集的功能进行精确描述,来确保不可达节点的正确回收和整个收集过程中内存堆数据保持和用户数据的不变性,保证了用户程序数据未被垃圾收集修改,也确保了用户程序没有干涉垃圾收集操作的正确执行。The garbage collection mechanism in Java effectively avoids some security vulnerabilities and improves resources utilisation rate as well. However for the garbage collection implemented in parallels with users program, its process and the realisation of the algorithm are so complicated, this makes the reliability is hard to be guaranteed. At present, the technology of programs dynamic analysis based on contract has become an important way to ensure the software quality. And the JML inherits all the advantages of contractual design and becomes a for- malised behaviour interface specification language tailored for Java, and is used to regulate the behaviour and the detailed design decision of Java program module. Based on such idea, in this paper we use preconditions, postconditions and other specifications to precisely describe the function of garbage collection, and to ensure the correct retrieval of the unreachable nodes and the retention of memory heap data and the invariance of user data. While ensuring users＇ data not being modified by the garbage collection, the program also guarantees there is no inter- ference from users program on the correct implementation of garbage collection operations.

关 键 词：契约试设计 Java建模语言 垃圾收集 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]