VeriJava中静态验证器的设计与实现

论文摘要

软件的可靠性一直是工业界和学术界关注的焦点,随着软件系统的规模和复杂度的不断增长,如何保证其可靠性成为了亟待解决的问题。软件开发方法和软件工程也在不断发展,当今主流的面向对象方法已经走过了20多个年头,它在提供给系统良好的灵活性和可复用性的同时,并没有忽略它的可靠性,契约式设计就是一种用于构建高可靠的面向对象软件系统的系统化方法。Bertrand Meyer在90年代提出了契约式设计,并且发明了Eiffel编程系统来大力推广这种方法。契约式设计中使用契约来检查程序正确性的方法来源于早期的程序验证思想,虽然其主要价值体现在其面向对象的设计方面,但是它的出现也为程序验证提供了一条新的途径。在21世纪初,图灵奖获得者C.A.R.Hoare将60年代提出的“验证编译器”(verifying compiler)的构想作为计算机科学的重大挑战重新提出,并且号召全世界范围内的计算机科学家参与到这个宏大的项目当中。本文介绍的VeriJava项目旨在构建一个全面支持契约式设计的面向对象编程系统。VeriJava是Verifiable Java的缩写,它通过针对Java语言在语言层面上进行的扩展,提供了程序契约的表达方法,并同时提供了一套动态检查和静态验证机制。本文重点研究了VeriJava项目中的静态验证器模块的设计和实

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 研究背景
• 1.1.1 课题的研究意义
• 1.1.2 国内外研究现状
• 1.2 研究内容
• 1.2.1 课题的研究目标
• 1.2.2 本文的工作
• 1.3 本文的内容组织
• 第二章 契约式设计与程序验证
• 2.1 契约式设计
• 2.2 程序验证
• 2.2.1 基于归纳断言的程序验证
• 2.2.2 契约式设计与程序验证
• 2.3 本章小结
• 第三章 VeriJava 项目介绍
• 3.1 VeriJava 整体方案
• 3.2 VeriJava 语言扩展
• 3.2.1 契约的表示方法
• 3.2.2 语言扩展的优缺点
• 3.3 VeriJava 编译器
• 3.4 本章小结
• 第四章 VeriJava 静态验证器的设计与实现
• 4.1 静态验证器的构架
• 4.2 前端翻译器
• 4.2.1 VeriJava 中的 Guarded Command 语言
• 4.2.2 从VeriJava 到Guarded Command 语言的转换
• 4.2.3 前端翻译器的设计与实现
• 4.3 验证条件生成器
• 4.3.1 从GC 语言到验证条件的转换
• 4.3.2 验证条件生成器的设计与实现
• 4.4 定理证明器
• 4.4.1 Simplify 定理证明器
• 4.4.2 VeriJava 中对 Simplify 的使用
• 4.5 后端处理器
• 4.6 本章小结
• 第五章 实验与评估
• 5.1 实验介绍
• 5.2 结果与评估
• 5.3 本章小结
• 第六章 全文总结
• 6.1 文章总结
• 6.2 展望
• 参考文献
• 附录 1:实验源代码
• 致谢
• 攻读学位期间发表的学术论文目录