劉 波，劉志明，裘宗燕,3，秦 曉

（1.西南大學 計算機與信息科學學院，重慶 400715；2.西南大學 軟件研究與創(chuàng)新中心，重慶 400715；3.北京大學 數(shù)學科學學院，北京 100871）

0 引 言

隨著信息、計算機、通訊技術（ICT）的高速發(fā)展及人類社會與文明的進步，計算機系統(tǒng)及軟件已深植各行業(yè)，未來智慧城市與智慧經濟將實現(xiàn)資源、能源分布式生產及集約化管理與使用。在這些愿景[1]中，各行業(yè)異構系統(tǒng)一體化與持續(xù)演化將是關鍵環(huán)節(jié)，而計算機系統(tǒng)的正確性與可信性是重中之重，在ACM和IEEE制定的計算機科學及軟件工程課程指南[2-3]中均包含文章探討的程序（軟件）正確性。軟件是人類構造的最復雜的工程產品，研究和實踐表明，保證軟件正確性沒有銀彈[4]，圖靈獎得主Sir Tony Hoare教授等把嚴格證明軟件正確性視為重大挑戰(zhàn)[5-6]。從1968年慕尼黑軟件工程會議算起，程序設計理論與方法、軟件工程過程、體系結構及其設計、驗證和確認等領域經過近50年的研究與實踐已取得長足進步，而程序（軟件）正確性正是這些理論和方法希望解決的首要問題。

1 程序正確性的內涵及意義

程序及軟件設計的知識與技術是計算機科學和軟件工程兩學科核心知識的交集，也構成了計算機本科專業(yè)教學大綱的核心[2-3]。程序正確性是其中的基礎概念，也是1968年慕尼黑召開第一次軟件工程會議就“解決軟件危機”所提出并討論的最重要概念和核心問題[7]。

程序（軟件）正確性是指程序能實現(xiàn)并滿足相關需求，包括所需計算功能以及功能與信息安全性、信息私密性等方面的要求；軟件的錯誤行為表現(xiàn)為系統(tǒng)的各種漏洞、缺陷和脆弱性，它們可能引發(fā)系統(tǒng)運行中的各種問題，甚至造成災難。2002年美國國家標準技術研究所的一項研究表明[8]，軟件缺陷每年給美國造成的經濟損失高達595億美元；軟件錯誤導致Therac-25放射醫(yī)療儀放射過量100倍，造成至少3人死亡（1985—1987）；軟件故障導致Ariane-5火箭爆炸事故（1996），造成直接損失高達3.7億歐元。

隨著計算機應用日漸廣泛，軟件故障已成為人們熟知且無奈接受的普遍問題。ICT領域的高速發(fā)展催生了物聯(lián)網、人工智能、大數(shù)據等大批新技術，但軟件缺陷和脆弱性問題日益嚴峻，近日爆發(fā)的勒索病毒就是其中的典型。而在實際生活中，很多軟件系統(tǒng)故障是不能接受的，諸多關鍵領域如政府管理、交通管理、銀行金融、電網管控、交通控制、醫(yī)療設備等的計算機系統(tǒng)，其漏洞和缺陷可能導致巨大災難、社會動蕩甚至難以挽回的重大損失。毋庸置疑，確保軟件正確性和質量是未來計算機工作者最重要的使命。

圖靈獎獲得者Lamport曾說“最好的軟件工具是訓練有素的頭腦”，正確可信軟件最重要的保障是可信的軟件工程師。眾多計算機專業(yè)學生直到畢業(yè)還不理解甚至完全不知道程序正確性及如何思考正確性相關問題，這給正確、安全的良好系統(tǒng)的產生帶來了障礙。程序正確性能力的培養(yǎng)有利于為計算機專業(yè)教育培養(yǎng)稱職的下一代計算機專業(yè)人員。

2 形式化方法

為應對軟件危機，以Floyd[9]、Hoare[10]、Sccot[11]、Dijkstra[12]、Plotkin[13]為代表的計算機科學家從20世紀60年代后期開始用數(shù)學和邏輯方法研究編程語言的形式語義，建立程序的嚴格描述（規(guī)約）、推理和證明，通過20余年的研究，奠定了形式語義學在計算機科學中的核心地位。在形式語義理論及其邏輯演算、自動機理論與形式語言、類型系統(tǒng)和抽象數(shù)據類型的基礎上，形成了基于數(shù)學的軟件系統(tǒng)規(guī)約、設計、開發(fā)和驗證的技術和方法，稱為（軟件工程的）形式化方法，旨在為軟硬件開發(fā)建立類似其他成熟工程領域的數(shù)學基礎，以有效分析和證明系統(tǒng)設計的正確性、可靠性和魯棒性等[14]。

2.1 形式化方法的發(fā)展和挑戰(zhàn)

形式化方法研究在20世紀的后30年非?；钴S，產生了許多與軟件正確性相關的概念、理論和方法，如正確性驗證、可組合設計和驗證、精化和抽象解釋等，構成了嚴格、清晰、系統(tǒng)地理解、表述及思考軟件正確性及系統(tǒng)設計的思想工具。與傳統(tǒng)的基于經驗和試錯的方法不同,形式化方法旨在為程序（軟件）設計建立科學基礎和系統(tǒng)工程方法論，其中提煉升華的概念和定律已成為程序設計的基本準則（如前置條件、后置條件、循環(huán)變式/不變式（variants/invariants）等；及其與程序正確性、程序或算法設計、分析和測試的關系），指導著現(xiàn)代的程序設計和軟件研發(fā)。

形式化方法能發(fā)現(xiàn)一些傳統(tǒng)方法難以發(fā)現(xiàn)的錯誤，在硬件領域的應用廣泛而深入，商品驗證工具已經相當成熟。國外許多半導體公司把形式化驗證納入基本開發(fā)流程，如ARM等已用JASPER形式驗證基本取代模擬驗證；還出現(xiàn)了專業(yè)的形式化驗證公司，如JASPER和Calypto，著名半導體公司（如INTEL、NVDIA、ARM）都是其客戶。2007年以來，JASPER年收益增長率為37%，為EDA工業(yè)平均水平的6倍，用戶數(shù)年增長率為79%，許可證增長率為129%，可處理規(guī)模的年增長率達100%，遠超摩爾定律的40%。

形式化方法在軟件領域的應用遇到很大挑戰(zhàn)，現(xiàn)有的形式化方法和工具尚難支持工業(yè)界大規(guī)模軟件系統(tǒng)開發(fā)，這也使有關研究與教育受到負面沖擊，中國計算機教育尤為顯著。新興熱門技術（如人工智能等）的不斷涌現(xiàn)及ICT行業(yè)的繁榮加劇了教育的現(xiàn)實主義情緒，忽視了作為基礎理論的形式化方法教育。然而，新興ICT熱點的涌現(xiàn)并沒有改變計算機科學和軟件工程的本質，隨著計算機應用的發(fā)展，系統(tǒng)的正確性和可靠性只會越來越重要，近年來的形式化領域的成果也證明其可能在系統(tǒng)開發(fā)中發(fā)揮重要作用。

2.2 近年一些重要成果

編譯器是最重要的系統(tǒng)軟件，但常用編譯器都未驗證，不能確保目標代碼與源代碼的語義一致性。2012年法國研究者發(fā)布了經過驗證的優(yōu)化編譯器CompCert，該編譯器用輔助證明系統(tǒng)Coq開發(fā)，嚴格證明了目標代碼與源程序的等價性。PLDI 2011上有一項用6年時間檢查在用編譯器錯誤的工作，只有當時CompCert里驗證過的部分沒發(fā)現(xiàn)錯誤，其他廣泛使用的編譯器如VC、gcc等都發(fā)現(xiàn)了錯誤。2015年MIT學者開發(fā)了經過驗證的文件系統(tǒng)FSCQ（SOSP 2015），可保證無論何時系統(tǒng)崩潰，重啟后都能正確恢復文件系統(tǒng)，不會丟失數(shù)據（稱為crash safety），有關原型系統(tǒng)可以在Linux上實際使用。

美國國防部的HACMS項目（high-assurance cyber military systems）研究如何開發(fā)高可信、黑客無法入侵的軍用系統(tǒng)，開發(fā)的無人機控制系統(tǒng)基于形式化驗證的OS內核sel4，通過了白帽黑客的攻擊試驗。耶魯大學開發(fā)了經過驗證的支持多核CPU的OS內核CertiKOS（OSDI’16）。B方法支持從抽象規(guī)范到代碼（C或Ada）生成的整個開發(fā)流程，已有工業(yè)級開發(fā)及證明工具。人們用B方法開發(fā)了數(shù)十條地鐵線路的自動駕駛系統(tǒng)，如巴黎地鐵14號線，還將其用于其他領域的安全攸關系統(tǒng)，如汽車和航空等領域。

在改進傳統(tǒng)軟件開發(fā)方面，形式化方法也取得了很多成果，如利用符號執(zhí)行技術分析重要程序（如Linux）并發(fā)現(xiàn)了許多錯誤；結合符號執(zhí)行和約束求解技術生成測試用例，幫助找出錯誤執(zhí)行路徑。微軟將驗證工具嵌入其設備驅動程序開發(fā)系統(tǒng)，幫助開發(fā)者檢查邏輯錯誤。還有軟件公司把基于形式化技術開發(fā)的工具應用于開發(fā)流程；相關理論研究也取得了許多成果，已開發(fā)出一批功能強大的驗證工具。

3 計算機專業(yè)基礎課程中的問題

筆者認為，計算機本科專業(yè)教育需要為計算機及其應用培養(yǎng)具有問題解決能力的、合格的開發(fā)和管理人才；培養(yǎng)具有進一步發(fā)展能力、創(chuàng)新能力和研發(fā)能力的工程技術人員；培養(yǎng)有潛力的、有志于繼續(xù)深造，可能從事相關科研和教學工作的畢業(yè)生?？紤]到計算機領域發(fā)展的需要，專業(yè)課程應該為學生提供計算機與軟件工業(yè)界及特定應用領域所需要的知識和技術，從而培養(yǎng)學生的實際問題解決能力，以保證畢業(yè)生就業(yè)；為學生提供支持長遠發(fā)展所需的核心概念與理論，相關能力與素質，如數(shù)學思維、計算思維、抽象思維[15]及嚴謹?shù)倪壿嬐评砟芰Α⒐こ淘O計和實施能力等；培養(yǎng)學生獨立思考、解決問題和自我學習與探索的能力和素質，包括協(xié)作精神和合作交流能力。關鍵的概念、理論、技術和方法都需要體現(xiàn)在課程內容中，尤其是作為基石的核心基礎理論，這其中就包括形式化方法，培養(yǎng)未來計算機工作者是一項綜合性工作，需要從基礎課程開始考慮。

3.1 CS1：計算機專業(yè)第一門課

CS1的主要內容是程序設計，旨在幫助學生建立計算概念，鍛煉基本編程能力，掌握一種編程語言，通過實踐掌握正確的程序設計方法，初步理解計算思維。

當前CS1中最重要的缺失是不討論程序是否正確。教科書和教學中通常用具體數(shù)據說明程序的執(zhí)行情況，這會讓學生認為編程就是一種通過初步設計和實現(xiàn)，而后試錯和修改的過程，目標是使程序通過一些數(shù)據的檢驗，計算機輔助編程練習系統(tǒng)進一步強化了這種錯誤觀念。圖靈獎獲得者Edsgar W. Dijkstra指出了測試的局限性：測試可以證明程序錯誤的存在，但不能證明其不存在。實際上，脫離了需求與正確性，不可能真正理解程序測試、缺陷診斷和缺陷修復，只有理解了程序的意義，理解程序語法結構和語義之間的關系，才能真正學會編程。

討論程序的正確性要有明確的問題需求，學生需要理解一些概念，學習如何分析問題，通過抽象和嚴格化得到準確的需求描述，才能真正理解程序。為嚴格說明一個程序部件（如函數(shù)）的需求，必須說明函數(shù)對參數(shù)的要求及產生的結果或效果，嚴格描述就得到了函數(shù)的前后置條件。此外，任何一段包含while循環(huán)的代碼，都可能有無窮多執(zhí)行情況（執(zhí)行路徑），這意味著不能給出完全的測試數(shù)據集，無法通過測試認定其正確性，需要引入循環(huán)不變式概念說明其正確性。程序的終止與否及并發(fā)程序死鎖和活鎖問題均依賴于循環(huán)語句的終止性，理解論證循環(huán)的終止性需要清楚循環(huán)變式。

3.2 CS2：計算機專業(yè)第二門課

CS2討論數(shù)據結構及相關問題，目前教學中普遍采用ADT的概念。要說明一個數(shù)據結構正確，須有數(shù)據不變式的概念，這是數(shù)據結構需求說明的核心，沒有它就無法說明一個數(shù)據結構的結構良好、初始化正確、操作的實現(xiàn)正確。此外，還需要證明不同操作之間相互配合，這些都需要形式化理論的支持。理解數(shù)據不變式的概念對學習面向對象程序設計也很重要，對象/類不變式可看作數(shù)據不變式的推廣，類不變式和類方法的前后置條件共同構成類合約（class contracts）的基礎[16]。

以循環(huán)順序表的隊列實現(xiàn)為例（圖1），該實現(xiàn)常用的是一個數(shù)組和兩個下標（或指針）變量，需要設定變量初值，在入隊和出隊操作時更新變量。只有初始化和操作正確配合才能實現(xiàn)隊列的功能，而這些配合就需要數(shù)據不變式的指導。更復雜的數(shù)據結構尤其如此，不掌握這種概念工具，就沒有學到數(shù)據結構設計的真諦。

圖1 循環(huán)順序表的隊列實現(xiàn)

3.3 程序正確性教育現(xiàn)狀的問卷調查與分析

針對程序正確性知識在我國計算機本科教育中的現(xiàn)狀所做的問卷調查共收到87所高校的有效反饋167份[17]，統(tǒng)計結果為：23.27%的高校（23所）開設自動機理論和形式語言課程（由于問題設計不夠精確，該數(shù)據有可能涵蓋了包含自動機內容的編譯原理等課程）； 25.16%的高校（25所）講授前置和后置條件概念；22.14%的高校（22所）講授循環(huán)不變式概念；30.19%的高校（30所）講授循環(huán)語句終止性概念和循環(huán)變式； 18.24%的高校（18所）開設函數(shù)程序設計課；18.24%的高校（18所）開設有形式化課程。

調查結果證實我國計算機本科教育和歐美中等以上計算機院系有不小差距。據網上查詢，美國CMU、Stanford、MIT、Cornel及英國Oxford、Cambridge、IC等頂尖大學的計算機本科大綱都把自動機與形式語言理論列為核心必修課，明確要求在程序設計、算法設計與分析、數(shù)據結構等課程中講授正確性的概念和思想。筆者劉志明曾在英國高校任教多年，了解Warwick、York、Newcastle及其曾任教的Leicester等大學本科都開設形式語義、形式化規(guī)約、并發(fā)和模型檢驗、函數(shù)程序設計等課程。

關于形式化重要性的問卷結果見表1。雖然問卷在CCF、CCF YOCSEF及多個專委會微信群分發(fā)，但反饋數(shù)量令人失望；反饋意見主要來自有形式化方法背景的專家學者，結果中對形式化方法的重要性有較高認可率。

表1 形式化方法及其基礎知識重要性統(tǒng)計結果 %

3.4 程序正確性教育對學生的重要性

在基礎課程中加入一些形式化概念的討論，能幫助學生正確理解計算機科學的本質，掌握正確的思考方法和設計技術，有助于學生的后續(xù)學習和未來工作，使其成長為超越前人的新一代計算機工作者。

目前常用的編程語言都有的斷言機制就是為了在代碼中明確地描述語義。CS1應該把這種機制作為專門問題，說明需要的原因、在程序開發(fā)中的作用、正確寫出的方法，要求學生在程序中寫出斷言，促使學生認真思考程序的行為，提高程序質量和可讀性；還可以結合斷言介紹程序的語義和正確性概念，包括環(huán)境和狀態(tài)等。實際上，狀態(tài)、環(huán)境、斷言、前置條件和后置條件、循環(huán)不變式、數(shù)據不變式等概念，已越來越多地出現(xiàn)在探討軟件技術的專業(yè)著作中，還有著作專門討論基于合約（contract）的程序開發(fā)，這說明軟件業(yè)界和開發(fā)專家都越來越重視程序正確性問題，計算機基礎課程必須反映這種趨勢。后續(xù)課程也應該討論相關的概念，如越來越多的應用涉及并發(fā)程序設計，測試技術特別需要理論指導；軟件工程討論系統(tǒng)建模，UML建模用到的狀態(tài)機和描述對象約束的OCL語言等都是形式化概念的應用。實際上，形式化技術已經在一些課程的領域取得了顯著成效，最典型的如編譯課程中詞法和語法的形式化描述，數(shù)據庫課程中的數(shù)據范式等。

加強有關程序正確性的討論，倡導嚴格的思想方法和設計過程，幫助學生掌握相關方法，加強嚴格性，有助于提高軟件質量。這些內容還可激發(fā)學生對深入學習和使用形式化方法的興趣，對于在軟件領域深造的研究生都會有很大幫助。開發(fā)自主創(chuàng)新的操作系統(tǒng)、程序設計語言和編譯器也要求彌補本科教育中程序正確性概念、思想和方法的缺失。

4 關于計算機專業(yè)教育加強學生對形式化方法認知的建議

各學校計算機專業(yè)應當研究如何結合自身情況，在課程設置、內容和授課方式等方面加強程序正確性方面的知識和技能傳授，有兩種方式可供選擇：①采取柔性、漸進方式改良基礎課核心知識和技能，這對大多數(shù)高校更現(xiàn)實可行；②增加專門的形式化方法課程。對此我們有如下建議：

（1）加強和改進現(xiàn)有“離散數(shù)學”課程，應充分挖掘集合論、數(shù)理邏輯、圖論等在計算機領域的實際應用，不能將其變?yōu)榧兇獾臄?shù)學課程。

（2）在基礎課程（從CS1和CS2開始）中采用嚴格、直觀的“非形式講授法”介紹程序正確性的概念和思維方式（有經驗顯示這樣做是可行且有效的[18]），包括但不限于程序語言的語法和語義的關系、程序狀態(tài)和環(huán)境；程序（或算法問題）需求、前置條件和后置條件（程序／算法的合約）；循環(huán)不變式、循環(huán)變式與終止等概念；如何在分析、設計、調試和測試中利用這些概念；如何從程序合約及循環(huán)不變式出發(fā)設計、導出或組合出程序；如何使用合約進行程序分析、測試、檢查和調試。

（3）建議開設形式語言與自動機課程，這是計算理論、語言設計和計算模型的核心基礎。

（4）后續(xù)課程也要特別介紹相關的理論概念和研究成果，提高學生的理論素養(yǎng)。如在編譯課介紹有窮自動機時，應說明其在軟件系統(tǒng)設計中的作用。在軟件工程中討論UML建模時，應嚴格講解各種UML模型的語法和語義（元模型）之間的關系，講解不同UML模型之間的關系、在軟件開發(fā)（需求模型、架構設計、交互的描述、集成、測試等）中的作用和一致性，介紹相關描述機制與計算機系統(tǒng)設計的關系和應用等。

（5）有條件的學校應考慮在本科開設有關形式化方法的初級課程，如形式化的系統(tǒng)建?；蚧诰唧w工具的嚴格軟件開發(fā)。

形式化方法的非形式講授不容易做好，教師需要對程序設計理論與方法有所了解。研究者們多年來開發(fā)了許多解決計算問題的理論工具，包括邏輯（命題邏輯和一階邏輯、Hoare邏輯等）、自動機及其擴展（如時間自動機、概率自動機）、進程代數(shù)（如CSP、CCS、Pi演算）、Petri網及其變形、形式文法技術（如正則語言、BNF）等，還有離散數(shù)學中的集合和圖論等，這些技術能用于嚴格描述和處理計算機領域的許多問題，也能為具體問題開發(fā)專用的記法形式提供參考。許多形式化描述有工具支持，可以幫助檢查錯誤，幫助早期發(fā)現(xiàn)設計錯誤，如前面介紹的B方法支持從抽象的系統(tǒng)描述生成代碼，基礎就是一階邏輯和集合論。教師應當對形式化描述和工具有所了解，嚴格分析和表述課程和開發(fā)中的問題；計算機學會尤其是形式化方法專委會，也應該考慮組織教師的研修活動，鼓勵編寫合適的教材。

5 結 語

計算機領域發(fā)展迅猛，新熱點層出不窮，工業(yè)界和社會對人才的需求緊迫、要求廣泛，需要在計算機核心基礎理論方面有很高造詣的弄潮兒，也需要扎實掌握計算機基礎知識體系與技能的合格水手，需要他們承擔起計算機科技與應用的發(fā)展和創(chuàng)新的重要使命，并能建設智慧城市、智慧經濟等系統(tǒng)為人類社會與文明可持續(xù)發(fā)展謀取福祉。搞好計算機專業(yè)教育是一個復雜的問題，見仁見智，但公認的宗旨是為未來培養(yǎng)稱職的下一代專業(yè)人員，期望文章提出的呼吁能引起同仁們對程序正確性的重視，開始更深入地思考和討論。

[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]劉波, 劉志明, 裘宗燕, 等. 本科形式化方法教育現(xiàn)狀調查問卷統(tǒng)計結果[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.