加強計算機本科專業程序正確性知識教育與能力培養

劉 波，劉志明，裘宗燕,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.