CAJ | 학술논문

Java中的垃圾收集机制，有效地避免了安全漏洞也提高了资源利用率。然而对于和用户程序并行执行的垃圾收集，其过程及算法的实现甚是复杂，使得可靠性难以保证。目前，基于契约的程序动态分析技术已成为软件质量保证的一个重要途径。而JML继承了契约式设计的所有优点，成为一种为Java 量身定做的形式化的行为接口规范语言，用来规范Java程序模块的行为及详细设计决策。基于这种思想，通过前置条件、后置条件等规范对垃圾收集的功能进行精确描述，来确保不可达节点的正确回收和整个收集过程中内存堆数据保持和用户数据的不变性，保证了用户程序数据未被垃圾收集修改，也确保了用户程序没有干涉垃圾收集操作的正确执行。
Java중적랄급수집궤제，유효지피면료안전루동야제고료자원이용솔。연이대우화용호정서병행집행적랄급수집，기과정급산법적실현심시복잡，사득가고성난이보증。목전，기우계약적정서동태분석기술이성위연건질량보증적일개중요도경。이JML계승료계약식설계적소유우점，성위일충위Java 량신정주적형식화적행위접구규범어언，용래규범Java정서모괴적행위급상세설계결책。기우저충사상，통과전치조건、후치조건등규범대랄급수집적공능진행정학묘술，래학보불가체절점적정학회수화정개수집과정중내존퇴수거보지화용호수거적불변성，보증료용호정서수거미피랄급수집수개，야학보료용호정서몰유간섭랄급수집조작적정학집행。
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 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.