加強(qiáng)計(jì)算機(jī)本科專業(yè)程序正確性知識(shí)教育與能力培養(yǎng)

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

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

0 引 言

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

1 程序正確性的內(nèi)涵及意義

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

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

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

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

2 形式化方法

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

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

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

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

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

2.2 近年一些重要成果

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

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

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

3 計(jì)算機(jī)專業(yè)基礎(chǔ)課程中的問(wèn)題

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

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

CS1的主要內(nèi)容是程序設(shè)計(jì)，旨在幫助學(xué)生建立計(jì)算概念，鍛煉基本編程能力，掌握一種編程語(yǔ)言，通過(guò)實(shí)踐掌握正確的程序設(shè)計(jì)方法，初步理解計(jì)算思維。

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

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

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

CS2討論數(shù)據(jù)結(jié)構(gòu)及相關(guān)問(wèn)題，目前教學(xué)中普遍采用ADT的概念。要說(shuō)明一個(gè)數(shù)據(jù)結(jié)構(gòu)正確，須有數(shù)據(jù)不變式的概念，這是數(shù)據(jù)結(jié)構(gòu)需求說(shuō)明的核心，沒(méi)有它就無(wú)法說(shuō)明一個(gè)數(shù)據(jù)結(jié)構(gòu)的結(jié)構(gòu)良好、初始化正確、操作的實(shí)現(xiàn)正確。此外，還需要證明不同操作之間相互配合，這些都需要形式化理論的支持。理解數(shù)據(jù)不變式的概念對(duì)學(xué)習(xí)面向?qū)ο蟪绦蛟O(shè)計(jì)也很重要，對(duì)象/類不變式可看作數(shù)據(jù)不變式的推廣，類不變式和類方法的前后置條件共同構(gòu)成類合約（class contracts）的基礎(chǔ)[16]。

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

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

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

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

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

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

表1 形式化方法及其基礎(chǔ)知識(shí)重要性統(tǒng)計(jì)結(jié)果 %

3.4 程序正確性教育對(duì)學(xué)生的重要性

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

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

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

4 關(guān)于計(jì)算機(jī)專業(yè)教育加強(qiáng)學(xué)生對(duì)形式化方法認(rèn)知的建議

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

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

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

（3）建議開(kāi)設(shè)形式語(yǔ)言與自動(dòng)機(jī)課程，這是計(jì)算理論、語(yǔ)言設(shè)計(jì)和計(jì)算模型的核心基礎(chǔ)。

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

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

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

5 結(jié) 語(yǔ)

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

[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)狀調(diào)查問(wèn)卷統(tǒng)計(jì)結(jié)果[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.