012049验证编译器初探.pdf

第 3 卷 第 2 期 2007 年 2 月 验证编译器初探 霍 玮 张兆庆 关键词：编译器 软件 中国科学院计算技术研究所 由于软件系统无一例外地都会存在着各种错 背景介绍 误和问题，因此，软件系统的可信性，作为软件 质量最重要的衡量标准之一，始终是困扰计算机 随着社会信息化的深入发展，计算系统逐 界的一个难题。从艾伦·图灵（Alan Turing）[26] 到 渐深入社会的各个领域，在日常的生产生活中 约翰·麦卡锡（John McCarthy）[19] ，从罗伯特 扮演着越来越重要的角色。软件系统作为计算 [10] 系统的主导，其正确性也越来越重要。著名的 ·佛洛伊德（Robert W. Floyd） 到托尼·霍尔 [12] 计算机科学家麦卡锡说：原则上，只有当一个 （Tony Hoare） ，众多学术大家的研究成果奠 定了提高软件系统可信度的基础。当前，最广 计算机程序的规约是形式化表达的并且程序被 泛使用的是测试的方法。但是，受惠于科技的 在数学上检测证明其符合这些规约时，这个程 发展和技术的积累，程序的验证方法又重新成 序才能交付用户[20] 。 为科研热点。不但学术界始终站在科研的第一 然而，实际软件产品与此要求依然相差很 线，工业界，尤其是以微软[4] 、英特尔、IBM等 远，从软件技术发展本身的角度看，软件的可 为代表的有实力的大型IT企业投入很大力量， 靠性亟需提高，软件技术面临着新的挑战。 进行相关科研攻关，并取得了一定的成果。欧 软件技术面临挑战 洲一些国家的政府也开始在方面投入经费进行 科研[30] 。这时，以托尼·霍尔为代表的科学家 “旧”的软件危机，产生于20世纪60年代 们提出了验证编译器这一重大挑战项目，希望 末，其根源是由于软件的复杂性和软件工程的 借此来攻克这一难题[13] 。 相对不成熟性。从那时起，很多软件项目的成 同时，编译技术经过半个世纪的发展，面 本和开发进度难以控制，软件质量低、不易理 对新的多核多线程体系结构的产生，也前进到 解并且很难维护，或者完成的项目不能符合预 了一个进一步发展的交叉路口。新的体系结构 先需求。同时，一些运行着的软件由于软件错 给软件可靠性本身提出了更高的要求。面对现 误造成了经济上的损失，更有甚者，一些具有 状，基于长期从事编译技术研究工作的积累， 严重缺陷的软件所引发的问题危及生命。 我们进行了编译技术应用的新探索，尝试用编 据2002年美国商务部国家标准和科技机构 译技术提供基础支撑，提高软件可靠性，构造 1 ）发布的研究报告，由于软件错误或存 （NIST 开发高可靠软件的集成环境，希望为程序员开 在的瑕疵，给美国每年造成595亿美元的经济 发软件系统提供切实可用的工具支持。 损失，约占当年GDP的1%。同时，该报告还指 1 National Institute of Standards and Technology，美国国家标准与技术研究院