垃圾收集已经普遍应用于主流的软件开发领域中,有效地避免了一些安全漏洞的同时提高了资源利用率。然而,垃圾收集自身都比较复杂,其算法设计和实现的可靠性往往难以保证。对于和用户程序并行执行的垃圾收集器,其交互过程变得更加复杂,可靠性也更难保证。然而垃圾收集过程中的任何错误或异常都会导致用户程序在运行时产生不可预测的结果。因此要确保用户程序的有效执行,势必对垃圾收集的可靠性和安全性进行严格地研究。JML是一种精确的形式化的行为接口规范语言,继承了契约式设计的所有优点,能够规范程序模块的行为及详细设计决策,同时可以利用自身开发的工具进行高效率的测试,从而有效地保证软件质量。本文首先从垃圾收集技术的基本概念和基本技术出发,深入浅出地分析了垃圾收集技术背后的运行机理及其在具体内存堆上的行为,利用三色抽象原则实现了标记-清扫垃圾收集算法。为了减少垃圾收集给用户程序带来的停顿,在此基础上对算法进行改进,采用逐步更新的写拦截器实现了渐进式垃圾收集。为了严格地验证垃圾收集的安全性和正确性,本文首先利用Daikon动态分析工具和ESC/JAVA静态检测工具辅助生成程序不变量,然后使用JML对垃圾收集与用户程序交互过程的安全规范进行精确描述,避免了使用自然语言产生的需求不精确、可能产生歧义的问题。本文通过JML运行时断言检测完成了垃圾收集和用户程序交互的自动化形式验证,证明了不可达节点的正确回收以及整个收集过程中内存堆的数据保持和用户数据的不变性,保证了用户程序没有干涉垃圾收集器的正确执行,同时也确保了用户程序数据未被垃圾收集修改。最后通过实际的例子对两种垃圾收集算法进行比较分析,结果表明渐进式垃圾收集器能够缩短中断时间并且降低内存需求量,有效地提高了垃圾收集的运行效率。