基于JML的标记-清扫垃圾收集验证.pdf

《基于JML的标记-清扫垃圾收集验证.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第31卷第9期计算机应用与软件Vo1．3lNo．92014年9月ComputerApplicationsandSoftwareSep．2014基于JML的标记一清扫垃圾收集验证宋玉婷孙文辉(北京交通大学计算机与信息技术学院北京100044)摘要Java中的垃圾收集机制，有效地避免了安全漏洞也提高了资源利用率。然而对于和用户程序并行执行的垃圾收集，其过程及算法的实现甚是复杂，使得可靠性难以保证。目前，基于契约的程序动态分析技术已成为软件质量保证的一个重要途径。而JML继承了契约式设计的所有优点，成为一种为Java量身定做的形式化的行为接口规范语言，用来规范Java程序模块的行为及详细设计

2、决策。基于这种思想，通过前置条件、后置条件等规范对垃圾收集的功能进行精确描述，来确保不可达节点的正确回收和整个收集过程中内存堆数据保持和用户数据的不变性，保证了用户程序数据未被垃圾收集修改，也确保了用户程序没有干涉垃圾收集操作的正确执行。关键词契约试设计Java建模语言垃圾收集中图分类号TP301文献标识码ADOI：10．3969／j．issn．1000-386x．2014．09．006MARK-AND—SWEEPGARBAGECOLLECTIoNVERIFICATIoNBASEDoNJMLSongYutingSunWenhui(DepartmentofComputerSciencea

3、ndTechnology，BeijingJiaotongUniversity，Beijing100044，China)AbstractThegarbagecollectionmechanisminJavaeffectivelyavoidssomesecurityvulnerabilitiesandimprovesresourcesutilisationrateaswel1．Howeverforthegarbagecollectionimplementedinparallelswithusersprogram，itsprocessandtherealisationofthealgorit

4、hmareSOcomplicated，thismakesthereliabilityishardtobeguaranteed．Atpresent，thetechnologyofprogramsdynamicanalysisbasedoncontracthasbecomeanimportantwaytoensurethesoftwarequality．AndtheJMLinheritsalltheadvantagesofcontractualdesignandbecomesafor—malisedbehaviourinterfacespecificationlanguagetailore

5、dforJava，andisusedtoregulatethebehaviourandthedetaileddesigndecisionofJavaprogrammodule．Basedonsuchidea，inthispaperweusepreconditions，postconditionsandotherspecificationstopreciselydescribethefunctionofgarbagecollection，andtoensurethecorrectretrievaloftheunreachablenodesandtheretentionofmemo~hea

6、pdataandtheinvarianceofuserdata．Whileensuringusers’datanotbeingmodifiedbythegarbagecollection，theprogramalsoguaranteesthereisnointer-ferencefromusersprogramonthecorectimplementationofgarbagecollectionoperations．KeywordsContractualdesignJavamodellinglanguage(JML)Garbagecollection来大家做了很多相关工作。其中一种十

7、分重要且被广泛应用的0引言程序设计方法就是基于契约的程序设计。JML就是DBC在Ja—va中的一种实现。JML是一种精确的形式规范描述语言，能准近年来，垃圾收集已经成为可靠、高效程序运行平台的一个确表达方法的功能需求，且JML在形式规范的基础上，可以利重要组成部分。Java中也采集了垃圾收集机制，它使得程序员用自身开发的工具进行高效率的测试。JML可精确地表达功能不需手工的释放内存，从而有效地避免了悬空指针访问、内存泄模块的行为规范，避免了使用