计算机应用与软件Issue(9)：32-36,5.DOI:10.3969/j.issn.1000-386x.2014.09.006
基于JML的标记-清扫垃圾收集验证
MARK-AND-SWEEP GARBAGE COLLECTION VERIFICATION BASED ON JML
宋玉婷 1孙文辉1
作者信息
- 1. 北京交通大学计算机与信息技术学院 北京 100044
- 折叠
摘要
Abstract
ThegarbagecollectionmechanisminJavaeffectivelyavoidssomesecurityvulnerabilitiesandimprovesresourcesutilisationrate 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 usersdata 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建模语言/垃圾收集Key words
Contractualdesign/Javamodellinglanguage(JML)/Garbagecollection分类
信息技术与安全科学引用本文复制引用
宋玉婷,孙文辉..基于JML的标记-清扫垃圾收集验证[J].计算机应用与软件,2014,(9):32-36,5.
