加强计算机本科专业程序正确性知识教育与能力培养

刘 波，刘志明，裘宗燕,3，秦 晓

（1.西南大学 计算机与信息科学学院，重庆 400715；2.西南大学 软件研究与创新中心，重庆 400715；3.北京大学 数学科学学院，北京 100871）

0 引 言

随着信息、计算机、通讯技术（ICT）的高速发展及人类社会与文明的进步，计算机系统及软件已深植各行业，未来智慧城市与智慧经济将实现资源、能源分布式生产及集约化管理与使用。在这些愿景[1]中，各行业异构系统一体化与持续演化将是关键环节，而计算机系统的正确性与可信性是重中之重，在ACM和IEEE制定的计算机科学及软件工程课程指南[2-3]中均包含文章探讨的程序（软件）正确性。软件是人类构造的最复杂的工程产品，研究和实践表明，保证软件正确性没有银弹[4]，图灵奖得主Sir Tony Hoare教授等把严格证明软件正确性视为重大挑战[5-6]。从1968年慕尼黑软件工程会议算起，程序设计理论与方法、软件工程过程、体系结构及其设计、验证和确认等领域经过近50年的研究与实践已取得长足进步，而程序（软件）正确性正是这些理论和方法希望解决的首要问题。

1 程序正确性的内涵及意义

程序及软件设计的知识与技术是计算机科学和软件工程两学科核心知识的交集，也构成了计算机本科专业教学大纲的核心[2-3]。程序正确性是其中的基础概念，也是1968年慕尼黑召开第一次软件工程会议就“解决软件危机”所提出并讨论的最重要概念和核心问题[7]。

程序（软件）正确性是指程序能实现并满足相关需求，包括所需计算功能以及功能与信息安全性、信息私密性等方面的要求；软件的错误行为表现为系统的各种漏洞、缺陷和脆弱性，它们可能引发系统运行中的各种问题，甚至造成灾难。2002年美国国家标准技术研究所的一项研究表明[8]，软件缺陷每年给美国造成的经济损失高达595亿美元；软件错误导致Therac-25放射医疗仪放射过量100倍，造成至少3人死亡（1985—1987）；软件故障导致Ariane-5火箭爆炸事故（1996），造成直接损失高达3.7亿欧元。

随着计算机应用日渐广泛，软件故障已成为人们熟知且无奈接受的普遍问题。ICT领域的高速发展催生了物联网、人工智能、大数据等大批新技术，但软件缺陷和脆弱性问题日益严峻，近日爆发的勒索病毒就是其中的典型。而在实际生活中，很多软件系统故障是不能接受的，诸多关键领域如政府管理、交通管理、银行金融、电网管控、交通控制、医疗设备等的计算机系统，其漏洞和缺陷可能导致巨大灾难、社会动荡甚至难以挽回的重大损失。毋庸置疑，确保软件正确性和质量是未来计算机工作者最重要的使命。

图灵奖获得者Lamport曾说“最好的软件工具是训练有素的头脑”，正确可信软件最重要的保障是可信的软件工程师。众多计算机专业学生直到毕业还不理解甚至完全不知道程序正确性及如何思考正确性相关问题，这给正确、安全的良好系统的产生带来了障碍。程序正确性能力的培养有利于为计算机专业教育培养称职的下一代计算机专业人员。

2 形式化方法

为应对软件危机，以Floyd[9]、Hoare[10]、Sccot[11]、Dijkstra[12]、Plotkin[13]为代表的计算机科学家从20世纪60年代后期开始用数学和逻辑方法研究编程语言的形式语义，建立程序的严格描述（规约）、推理和证明，通过20余年的研究，奠定了形式语义学在计算机科学中的核心地位。在形式语义理论及其逻辑演算、自动机理论与形式语言、类型系统和抽象数据类型的基础上，形成了基于数学的软件系统规约、设计、开发和验证的技术和方法，称为（软件工程的）形式化方法，旨在为软硬件开发建立类似其他成熟工程领域的数学基础，以有效分析和证明系统设计的正确性、可靠性和鲁棒性等[14]。

2.1 形式化方法的发展和挑战

形式化方法研究在20世纪的后30年非常活跃，产生了许多与软件正确性相关的概念、理论和方法，如正确性验证、可组合设计和验证、精化和抽象解释等，构成了严格、清晰、系统地理解、表述及思考软件正确性及系统设计的思想工具。与传统的基于经验和试错的方法不同,形式化方法旨在为程序（软件）设计建立科学基础和系统工程方法论，其中提炼升华的概念和定律已成为程序设计的基本准则（如前置条件、后置条件、循环变式/不变式（variants/invariants）等；及其与程序正确性、程序或算法设计、分析和测试的关系），指导着现代的程序设计和软件研发。

形式化方法能发现一些传统方法难以发现的错误，在硬件领域的应用广泛而深入，商品验证工具已经相当成熟。国外许多半导体公司把形式化验证纳入基本开发流程，如ARM等已用JASPER形式验证基本取代模拟验证；还出现了专业的形式化验证公司，如JASPER和Calypto，著名半导体公司（如INTEL、NVDIA、ARM）都是其客户。2007年以来，JASPER年收益增长率为37%，为EDA工业平均水平的6倍，用户数年增长率为79%，许可证增长率为129%，可处理规模的年增长率达100%，远超摩尔定律的40%。

形式化方法在软件领域的应用遇到很大挑战，现有的形式化方法和工具尚难支持工业界大规模软件系统开发，这也使有关研究与教育受到负面冲击，中国计算机教育尤为显著。新兴热门技术（如人工智能等）的不断涌现及ICT行业的繁荣加剧了教育的现实主义情绪，忽视了作为基础理论的形式化方法教育。然而，新兴ICT热点的涌现并没有改变计算机科学和软件工程的本质，随着计算机应用的发展，系统的正确性和可靠性只会越来越重要，近年来的形式化领域的成果也证明其可能在系统开发中发挥重要作用。

2.2 近年一些重要成果

编译器是最重要的系统软件，但常用编译器都未验证，不能确保目标代码与源代码的语义一致性。2012年法国研究者发布了经过验证的优化编译器CompCert，该编译器用辅助证明系统Coq开发，严格证明了目标代码与源程序的等价性。PLDI 2011上有一项用6年时间检查在用编译器错误的工作，只有当时CompCert里验证过的部分没发现错误，其他广泛使用的编译器如VC、gcc等都发现了错误。2015年MIT学者开发了经过验证的文件系统FSCQ（SOSP 2015），可保证无论何时系统崩溃，重启后都能正确恢复文件系统，不会丢失数据（称为crash safety），有关原型系统可以在Linux上实际使用。

美国国防部的HACMS项目（high-assurance cyber military systems）研究如何开发高可信、黑客无法入侵的军用系统，开发的无人机控制系统基于形式化验证的OS内核sel4，通过了白帽黑客的攻击试验。耶鲁大学开发了经过验证的支持多核CPU的OS内核CertiKOS（OSDI’16）。B方法支持从抽象规范到代码（C或Ada）生成的整个开发流程，已有工业级开发及证明工具。人们用B方法开发了数十条地铁线路的自动驾驶系统，如巴黎地铁14号线，还将其用于其他领域的安全攸关系统，如汽车和航空等领域。

在改进传统软件开发方面，形式化方法也取得了很多成果，如利用符号执行技术分析重要程序（如Linux）并发现了许多错误；结合符号执行和约束求解技术生成测试用例，帮助找出错误执行路径。微软将验证工具嵌入其设备驱动程序开发系统，帮助开发者检查逻辑错误。还有软件公司把基于形式化技术开发的工具应用于开发流程；相关理论研究也取得了许多成果，已开发出一批功能强大的验证工具。

3 计算机专业基础课程中的问题

笔者认为，计算机本科专业教育需要为计算机及其应用培养具有问题解决能力的、合格的开发和管理人才；培养具有进一步发展能力、创新能力和研发能力的工程技术人员；培养有潜力的、有志于继续深造，可能从事相关科研和教学工作的毕业生。考虑到计算机领域发展的需要，专业课程应该为学生提供计算机与软件工业界及特定应用领域所需要的知识和技术，从而培养学生的实际问题解决能力，以保证毕业生就业；为学生提供支持长远发展所需的核心概念与理论，相关能力与素质，如数学思维、计算思维、抽象思维[15]及严谨的逻辑推理能力、工程设计和实施能力等；培养学生独立思考、解决问题和自我学习与探索的能力和素质，包括协作精神和合作交流能力。关键的概念、理论、技术和方法都需要体现在课程内容中，尤其是作为基石的核心基础理论，这其中就包括形式化方法，培养未来计算机工作者是一项综合性工作，需要从基础课程开始考虑。

3.1 CS1：计算机专业第一门课

CS1的主要内容是程序设计，旨在帮助学生建立计算概念，锻炼基本编程能力，掌握一种编程语言，通过实践掌握正确的程序设计方法，初步理解计算思维。

当前CS1中最重要的缺失是不讨论程序是否正确。教科书和教学中通常用具体数据说明程序的执行情况，这会让学生认为编程就是一种通过初步设计和实现，而后试错和修改的过程，目标是使程序通过一些数据的检验，计算机辅助编程练习系统进一步强化了这种错误观念。图灵奖获得者Edsgar W. Dijkstra指出了测试的局限性：测试可以证明程序错误的存在，但不能证明其不存在。实际上，脱离了需求与正确性，不可能真正理解程序测试、缺陷诊断和缺陷修复，只有理解了程序的意义，理解程序语法结构和语义之间的关系，才能真正学会编程。

讨论程序的正确性要有明确的问题需求，学生需要理解一些概念，学习如何分析问题，通过抽象和严格化得到准确的需求描述，才能真正理解程序。为严格说明一个程序部件（如函数）的需求，必须说明函数对参数的要求及产生的结果或效果，严格描述就得到了函数的前后置条件。此外，任何一段包含while循环的代码，都可能有无穷多执行情况（执行路径），这意味着不能给出完全的测试数据集，无法通过测试认定其正确性，需要引入循环不变式概念说明其正确性。程序的终止与否及并发程序死锁和活锁问题均依赖于循环语句的终止性，理解论证循环的终止性需要清楚循环变式。

3.2 CS2：计算机专业第二门课

CS2讨论数据结构及相关问题，目前教学中普遍采用ADT的概念。要说明一个数据结构正确，须有数据不变式的概念，这是数据结构需求说明的核心，没有它就无法说明一个数据结构的结构良好、初始化正确、操作的实现正确。此外，还需要证明不同操作之间相互配合，这些都需要形式化理论的支持。理解数据不变式的概念对学习面向对象程序设计也很重要，对象/类不变式可看作数据不变式的推广，类不变式和类方法的前后置条件共同构成类合约（class contracts）的基础[16]。

以循环顺序表的队列实现为例（图1），该实现常用的是一个数组和两个下标（或指针）变量，需要设定变量初值，在入队和出队操作时更新变量。只有初始化和操作正确配合才能实现队列的功能，而这些配合就需要数据不变式的指导。更复杂的数据结构尤其如此，不掌握这种概念工具，就没有学到数据结构设计的真谛。

图1 循环顺序表的队列实现

3.3 程序正确性教育现状的问卷调查与分析

针对程序正确性知识在我国计算机本科教育中的现状所做的问卷调查共收到87所高校的有效反馈167份[17]，统计结果为：23.27%的高校（23所）开设自动机理论和形式语言课程（由于问题设计不够精确，该数据有可能涵盖了包含自动机内容的编译原理等课程）； 25.16%的高校（25所）讲授前置和后置条件概念；22.14%的高校（22所）讲授循环不变式概念；30.19%的高校（30所）讲授循环语句终止性概念和循环变式； 18.24%的高校（18所）开设函数程序设计课；18.24%的高校（18所）开设有形式化课程。

调查结果证实我国计算机本科教育和欧美中等以上计算机院系有不小差距。据网上查询，美国CMU、Stanford、MIT、Cornel及英国Oxford、Cambridge、IC等顶尖大学的计算机本科大纲都把自动机与形式语言理论列为核心必修课，明确要求在程序设计、算法设计与分析、数据结构等课程中讲授正确性的概念和思想。笔者刘志明曾在英国高校任教多年，了解Warwick、York、Newcastle及其曾任教的Leicester等大学本科都开设形式语义、形式化规约、并发和模型检验、函数程序设计等课程。

关于形式化重要性的问卷结果见表1。虽然问卷在CCF、CCF YOCSEF及多个专委会微信群分发，但反馈数量令人失望；反馈意见主要来自有形式化方法背景的专家学者，结果中对形式化方法的重要性有较高认可率。

表1 形式化方法及其基础知识重要性统计结果 %

3.4 程序正确性教育对学生的重要性

在基础课程中加入一些形式化概念的讨论，能帮助学生正确理解计算机科学的本质，掌握正确的思考方法和设计技术，有助于学生的后续学习和未来工作，使其成长为超越前人的新一代计算机工作者。

目前常用的编程语言都有的断言机制就是为了在代码中明确地描述语义。CS1应该把这种机制作为专门问题，说明需要的原因、在程序开发中的作用、正确写出的方法，要求学生在程序中写出断言，促使学生认真思考程序的行为，提高程序质量和可读性；还可以结合断言介绍程序的语义和正确性概念，包括环境和状态等。实际上，状态、环境、断言、前置条件和后置条件、循环不变式、数据不变式等概念，已越来越多地出现在探讨软件技术的专业著作中，还有著作专门讨论基于合约（contract）的程序开发，这说明软件业界和开发专家都越来越重视程序正确性问题，计算机基础课程必须反映这种趋势。后续课程也应该讨论相关的概念，如越来越多的应用涉及并发程序设计，测试技术特别需要理论指导；软件工程讨论系统建模，UML建模用到的状态机和描述对象约束的OCL语言等都是形式化概念的应用。实际上，形式化技术已经在一些课程的领域取得了显著成效，最典型的如编译课程中词法和语法的形式化描述，数据库课程中的数据范式等。

加强有关程序正确性的讨论，倡导严格的思想方法和设计过程，帮助学生掌握相关方法，加强严格性，有助于提高软件质量。这些内容还可激发学生对深入学习和使用形式化方法的兴趣，对于在软件领域深造的研究生都会有很大帮助。开发自主创新的操作系统、程序设计语言和编译器也要求弥补本科教育中程序正确性概念、思想和方法的缺失。

4 关于计算机专业教育加强学生对形式化方法认知的建议

各学校计算机专业应当研究如何结合自身情况，在课程设置、内容和授课方式等方面加强程序正确性方面的知识和技能传授，有两种方式可供选择：①采取柔性、渐进方式改良基础课核心知识和技能，这对大多数高校更现实可行；②增加专门的形式化方法课程。对此我们有如下建议：

（1）加强和改进现有“离散数学”课程，应充分挖掘集合论、数理逻辑、图论等在计算机领域的实际应用，不能将其变为纯粹的数学课程。

（2）在基础课程（从CS1和CS2开始）中采用严格、直观的“非形式讲授法”介绍程序正确性的概念和思维方式（有经验显示这样做是可行且有效的[18]），包括但不限于程序语言的语法和语义的关系、程序状态和环境；程序（或算法问题）需求、前置条件和后置条件（程序／算法的合约）；循环不变式、循环变式与终止等概念；如何在分析、设计、调试和测试中利用这些概念；如何从程序合约及循环不变式出发设计、导出或组合出程序；如何使用合约进行程序分析、测试、检查和调试。

（3）建议开设形式语言与自动机课程，这是计算理论、语言设计和计算模型的核心基础。

（4）后续课程也要特别介绍相关的理论概念和研究成果，提高学生的理论素养。如在编译课介绍有穷自动机时，应说明其在软件系统设计中的作用。在软件工程中讨论UML建模时，应严格讲解各种UML模型的语法和语义（元模型）之间的关系，讲解不同UML模型之间的关系、在软件开发（需求模型、架构设计、交互的描述、集成、测试等）中的作用和一致性，介绍相关描述机制与计算机系统设计的关系和应用等。

（5）有条件的学校应考虑在本科开设有关形式化方法的初级课程，如形式化的系统建模或基于具体工具的严格软件开发。

形式化方法的非形式讲授不容易做好，教师需要对程序设计理论与方法有所了解。研究者们多年来开发了许多解决计算问题的理论工具，包括逻辑（命题逻辑和一阶逻辑、Hoare逻辑等）、自动机及其扩展（如时间自动机、概率自动机）、进程代数（如CSP、CCS、Pi演算）、Petri网及其变形、形式文法技术（如正则语言、BNF）等，还有离散数学中的集合和图论等，这些技术能用于严格描述和处理计算机领域的许多问题，也能为具体问题开发专用的记法形式提供参考。许多形式化描述有工具支持，可以帮助检查错误，帮助早期发现设计错误，如前面介绍的B方法支持从抽象的系统描述生成代码，基础就是一阶逻辑和集合论。教师应当对形式化描述和工具有所了解，严格分析和表述课程和开发中的问题；计算机学会尤其是形式化方法专委会，也应该考虑组织教师的研修活动，鼓励编写合适的教材。

5 结 语

计算机领域发展迅猛，新热点层出不穷，工业界和社会对人才的需求紧迫、要求广泛，需要在计算机核心基础理论方面有很高造诣的弄潮儿，也需要扎实掌握计算机基础知识体系与技能的合格水手，需要他们承担起计算机科技与应用的发展和创新的重要使命，并能建设智慧城市、智慧经济等系统为人类社会与文明可持续发展谋取福祉。搞好计算机专业教育是一个复杂的问题，见仁见智，但公认的宗旨是为未来培养称职的下一代专业人员，期望文章提出的呼吁能引起同仁们对程序正确性的重视，开始更深入地思考和讨论。

[1]Schaffers H, Komninos N, Pallo M, et al.Smart cities and The future internet: towards cooperation frameworks for open innovation[EB/OL]. [2017-12-29]. https://link.springer.com/chapter110.1007%2F978-3-642-20898-0-31.

[2]Joint Task Force on Computing Curricula (ACM and IEEE).Software engineering 2014: Curriculum guidelines for undergraduate degree programs in software engineering[M].New York: ACM, 2014: 10-19.

[3]Joint Task Force on Computing Curricula (ACM and IEEE). Computer science curricula 2013: Curriculum guidelines for undergraduate degree programs in computer science[M].New York: ACM, 2013: 27-38.

[4]Randell B, Buxton J. Software engineering: Report of a conference sponsored by the nato science committee[M]. Brussels: Scientific Aあairs Division, 1969: 1-130.

[5]Gang T. A collection of well-known software failures [EB/OL].(2016-08-26)[2017-05-10].http://www.cse.lehigh.edu/～gtan/bug/softwarebug.html.

[6]Brooks F. No silver bullet:Essence and accidents of software engineering[J]. Los Alamitos: IEEE Computer Society Press, 1987,20(4): 10-19.

[7]Hoare C, Misra J. Verified software:Theories,tools and experiments of a grand challenge project [C]//IFIP working conference on verified software: Theories, tools and experiments (VSTTE). Zurich: Revised Selected Papers and Discussions DBLP, 2005: 1-11.

[8]Hoare C. The verifying compiler: A grand challenge for computer research[J]. Journal of the ACM, 2003, 50(1): 63-69.

[9]Floyd R. Assigning meaning to programs[J]. Schwartz Jt Proc Symposium in Applied Mathematics, 1967(1): 19-32.

[10]Hoare C. An axiomatic basis for computer programming[J].Communications of the ACM, 1969, 12(10): 576-580.

[11]Scott D, Strachey C.Toward a mathematical semantics for computer languages[M]. Oxford: Oxford University Press, 1971: 1-50.

[12]Dijkstra E. A discipline of programming[J]. 1976, 12(4): 2719-2722.

[13]Plotkin G D. A structural approach to operational semantics[J]. The Journal of Logic and Algebraic Programming, 2004(7): 60-61.

[14]Holloway C M. Why engineers should consider formal methods[C]//Proceedings of 16th AIAA/IEEE on Digital Avionics Systems Conference(16th DASC). Irvine: IEEE, 1997: 16-22.

[15]Wing J M. Computational thinking [J].Communications of The ACM, 2006, 49(3): 33-35.

[16]Meyer B. Design by contract,in advances in object-oriented software engineering[M]. Upper Saddle River: Prentice Hall, 1991: 1-50.

[17]刘波, 刘志明, 裘宗燕, 等. 本科形式化方法教育现状调查问卷统计结果[EB/OL]. [2017-05-17]. http://www.swu-rise.net.cn/technical_report/Results_of_UFMES_Questionnaire.pdf.

[18]Morgan C. (In)-formal methods: The lost art[J]. Engineering Trustworthy Software Systems, 2014(9): 1-79.