高校計(jì)算機(jī)專(zhuān)業(yè)形式化方法課程教學(xué)研究

李均濤

［摘要］高校計(jì)算機(jī)專(zhuān)業(yè)開(kāi)設(shè)形式化方法課程十分必要。必須設(shè)計(jì)課程目標(biāo)和教學(xué)方法，并提出考核和評(píng)價(jià)學(xué)生學(xué)習(xí)效果的標(biāo)準(zhǔn)，通過(guò)嚴(yán)格的數(shù)學(xué)方法讓學(xué)生獲取對(duì)其他課程也很有益的知識(shí)、技術(shù)和能力。

［關(guān)鍵詞］形式化方法課程教學(xué)行為時(shí)序邏輯系統(tǒng)描述

［中圖分類(lèi)號(hào)］G423［文獻(xiàn)標(biāo)識(shí)碼］A［文章編號(hào)］2095-3437（2012）02-0073-02

軟件的可靠性是人們最為關(guān)注的一個(gè)性質(zhì)，尤其是對(duì)那些安全攸關(guān)的系統(tǒng)。為了使開(kāi)發(fā)的軟件系統(tǒng)更加可靠和安全，形式化方法應(yīng)運(yùn)而生且前景廣闊，也越來(lái)越引起計(jì)算機(jī)科學(xué)界的關(guān)注。[1]在此背景下，許多科學(xué)協(xié)會(huì)如國(guó)際計(jì)算機(jī)協(xié)會(huì)、電子與電氣工程師協(xié)會(huì)以及英國(guó)計(jì)算機(jī)協(xié)會(huì)都將形式化方法列為計(jì)算機(jī)科學(xué)本科教育的應(yīng)開(kāi)課程之一。[2]

本文將探討形式化方法課程在計(jì)算機(jī)科學(xué)本科教學(xué)中的雙重作用。此課程對(duì)計(jì)算機(jī)專(zhuān)業(yè)的本科生來(lái)說(shuō)，不僅可以增長(zhǎng)知識(shí)，更重要的是，可以提高學(xué)生更精準(zhǔn)地描述事物的能力和技巧。

一、課程目標(biāo)

形式化方法指的是各種數(shù)學(xué)建模技術(shù)，主要用于計(jì)算機(jī)系統(tǒng)行為的描述、建模，驗(yàn)證所設(shè)計(jì)的系統(tǒng)功能是否滿足設(shè)計(jì)需求和安全性。這些描述和驗(yàn)證可以按照不同的精確度來(lái)進(jìn)行。

形式化描述就是使用源自形式邏輯的標(biāo)記方法來(lái)刻畫(huà)需要建模的實(shí)際系統(tǒng)，包括系統(tǒng)的功能和這些功能的實(shí)現(xiàn)。

目前，歐美很多傳統(tǒng)大學(xué)的計(jì)算機(jī)系開(kāi)設(shè)了形式化方法課程，我國(guó)本科院校的計(jì)算機(jī)專(zhuān)業(yè)也已經(jīng)開(kāi)始跟進(jìn)。這些課程大部分包含了形式化描述和形式化驗(yàn)證兩部分，一般也會(huì)包含一個(gè)寬度優(yōu)先搜索方法的內(nèi)容。然而在形式化方法課程中，安排一種具體的形式化描述方法進(jìn)行深入學(xué)習(xí)更為合適。主要原因如下：首先，計(jì)算機(jī)專(zhuān)業(yè)的本科生要理解數(shù)學(xué)和數(shù)學(xué)建模在計(jì)算機(jī)科學(xué)中的重要地位非常困難，要有一個(gè)漸進(jìn)的過(guò)程。其次，形式化描述在某種程度上可以認(rèn)為是程序設(shè)計(jì)的數(shù)學(xué)抽象，而學(xué)生在程序設(shè)計(jì)以及面向?qū)ο蠓椒ê拖到y(tǒng)設(shè)計(jì)分析等課程中，已經(jīng)有了一定基礎(chǔ)，學(xué)起來(lái)會(huì)更容易，且更有利于學(xué)生理解形式化描述在軟件生命周期中的重要作用。最后，在學(xué)完本門(mén)課程后，學(xué)生可以基本掌握一種形式化描述的工具和方法，有助于學(xué)生對(duì)形式化方法的深入理解。

在這樣的定位下，本課程的目標(biāo)可以總結(jié)為：

第一，糾正學(xué)生“系統(tǒng)開(kāi)發(fā)就是編寫(xiě)代碼”的錯(cuò)誤認(rèn)識(shí)，明確形式化描述在精確刻畫(huà)系統(tǒng)和可靠系統(tǒng)開(kāi)發(fā)中的重要意義。第二，理解可靠系統(tǒng)的開(kāi)發(fā)過(guò)程。形式化描述可以通過(guò)發(fā)現(xiàn)不一致性和歧義性，為更好地理解可靠系統(tǒng)發(fā)揮重要作用。第三，認(rèn)識(shí)在系統(tǒng)開(kāi)發(fā)的初期發(fā)現(xiàn)不一致性對(duì)于系統(tǒng)開(kāi)發(fā)的重要性。第四，掌握一種形式化建模語(yǔ)言，可以為系統(tǒng)設(shè)計(jì)完整的、結(jié)構(gòu)良好的數(shù)學(xué)模型。本文將以行為時(shí)序邏輯及其描述語(yǔ)言TLA+為例。[3]第五，培養(yǎng)學(xué)生的抽象能力。形式化描述實(shí)際上就是對(duì)現(xiàn)實(shí)系統(tǒng)或?qū)⒁O(shè)計(jì)系統(tǒng)的一種數(shù)學(xué)抽象，它可以不關(guān)心系統(tǒng)細(xì)節(jié)的具體實(shí)現(xiàn)。在教學(xué)中，學(xué)生將學(xué)會(huì)如何對(duì)現(xiàn)實(shí)系統(tǒng)進(jìn)行數(shù)學(xué)抽象。

二、描述語(yǔ)言的選擇

對(duì)本門(mén)課程的設(shè)計(jì)，不能只是簡(jiǎn)單地教授描述語(yǔ)言的使用，更重要的是要讓學(xué)生學(xué)會(huì)如何進(jìn)行數(shù)學(xué)建模，包括如何進(jìn)行抽象和解決問(wèn)題。我們選擇了TLA+作為載體，因?yàn)樗兄趯?shí)現(xiàn)我們的目標(biāo)。

TLA是由美國(guó)科學(xué)家蘭帕德（Leslie Lamport）提出的一種用來(lái)規(guī)約和推理并發(fā)系統(tǒng)的邏輯。它基于線性時(shí)序邏輯（LTL），通過(guò)對(duì)行為及各種操作符的擴(kuò)展定義，可實(shí)現(xiàn)對(duì)并發(fā)系統(tǒng)及其性質(zhì)的描述與驗(yàn)證。它最突出的特點(diǎn)是：系統(tǒng)及其性質(zhì)可同時(shí)使用TLA公式來(lái)描述。基于TLA的描述語(yǔ)言TLA+以及模型檢測(cè)工具箱TLA ToolBox已經(jīng)成為獨(dú)具特色的形式化驗(yàn)證工具。

TLA+整合了線性時(shí)序邏輯、行為時(shí)序邏輯以及部分集論的內(nèi)容，是一種表達(dá)能力很強(qiáng)的形式化描述語(yǔ)言，并且非常簡(jiǎn)潔，很多龐大而又復(fù)雜的系統(tǒng)僅需一兩頁(yè)代碼即可完成建模。[4]

之所以選取TLA+作為描述語(yǔ)言，主要基于以下幾個(gè)方面的考慮：第一，TLA+已經(jīng)成為一個(gè)應(yīng)用較為普遍的形式化描述語(yǔ)言，不僅在學(xué)術(shù)界，而且目前在工業(yè)生產(chǎn)中也有了相當(dāng)普遍的應(yīng)用；第二，學(xué)生在之前已經(jīng)學(xué)習(xí)了邏輯和集論的數(shù)學(xué)概念，這些概念是學(xué)習(xí)TLA+的基礎(chǔ)；第三，學(xué)習(xí)TLA+可以讓學(xué)生掌握對(duì)現(xiàn)實(shí)系統(tǒng)的過(guò)程抽象和數(shù)據(jù)抽象方法，使得學(xué)生能從實(shí)際系統(tǒng)的運(yùn)行和具體數(shù)據(jù)的表示中抽離出來(lái)，更關(guān)注系統(tǒng)的整體框架，掌握抽象的步驟和方法；第四，TLA+使用了結(jié)機(jī)構(gòu)化和面向?qū)ο蟮姆椒?，這對(duì)學(xué)生鞏固以前的程序設(shè)計(jì)課程也是一個(gè)不小的幫助；第五，TLA+還具備一個(gè)正在不斷完善的集成開(kāi)發(fā)環(huán)境TLA ToolBox，可以對(duì)建立的模型進(jìn)行檢測(cè)和驗(yàn)證，為學(xué)生理解和進(jìn)一步學(xué)習(xí)形式化驗(yàn)證打下基礎(chǔ)。

三、教學(xué)和評(píng)價(jià)方法

作為專(zhuān)業(yè)限選課，我們將本課程安排在大學(xué)三年級(jí)第一學(xué)期，總課時(shí)數(shù)為36學(xué)時(shí)，包括課堂教學(xué)和輔導(dǎo)。

（一）教學(xué)方法設(shè)計(jì)

為了實(shí)現(xiàn)課程教學(xué)目標(biāo)，增強(qiáng)學(xué)生推理和解決問(wèn)題的技巧和能力，我們采用以下教學(xué)方法：

1.主動(dòng)學(xué)習(xí)

班級(jí)人數(shù)控制在40人以內(nèi)，保持一個(gè)較低的師生比，有利于形成主動(dòng)學(xué)習(xí)的氛圍。

2.啟發(fā)式教學(xué)

每當(dāng)開(kāi)始學(xué)習(xí)一個(gè)新的知識(shí)點(diǎn)，先介紹有關(guān)概念，然后利用一個(gè)實(shí)例來(lái)說(shuō)明如何使用TLA+進(jìn)行描述。當(dāng)然，對(duì)實(shí)例的描述并不是通過(guò)教師的講解來(lái)完成，而是由教師提出關(guān)鍵的、有啟發(fā)作用的問(wèn)題，然后引導(dǎo)學(xué)生自己寫(xiě)出形式描述語(yǔ)句。這樣學(xué)生就可以積極地參與到形式化描述的過(guò)程中，而不是被動(dòng)地接受信息，這樣效果會(huì)更好。

3.分組競(jìng)賽

將班級(jí)學(xué)生隨機(jī)分成由3～4人組成的學(xué)習(xí)小組，分別完成不同的案例。這些案例用自然語(yǔ)言給出，且故意包含一些模棱兩可的詞語(yǔ)，讓學(xué)生在編寫(xiě)形式化描述時(shí)去發(fā)現(xiàn)。然后每個(gè)小組推舉一人與教師進(jìn)行討論，讓學(xué)生明白形式化描述與自然語(yǔ)言描述的區(qū)別及其重要性。最后由教師對(duì)完成情況進(jìn)行點(diǎn)評(píng)，活躍課堂氣氛，提高學(xué)生的學(xué)習(xí)積極性。

4.反向思考

在輔導(dǎo)課上給出一些TLA+描述的系統(tǒng)，要求學(xué)生用自然語(yǔ)言對(duì)其進(jìn)行理解和解釋。這種方法可以讓學(xué)生了解一個(gè)好的軟件開(kāi)發(fā)者不僅要會(huì)設(shè)計(jì)程序，也必須會(huì)閱讀和理解系統(tǒng)描述。

5.注重全局

本課程從一開(kāi)始就引導(dǎo)學(xué)生使用TLA+建立系統(tǒng)架構(gòu)的形式模型，其中包括如何閱讀自然語(yǔ)言描述的系統(tǒng)需求，定義各種系統(tǒng)行為和性質(zhì)，以及用行為和性質(zhì)構(gòu)建系統(tǒng)模型的時(shí)序邏輯公式。這種方法有助于學(xué)生建立良好的大局觀，對(duì)今后設(shè)計(jì)系統(tǒng)的總體框架打下堅(jiān)實(shí)的基礎(chǔ)。

（二）課程內(nèi)容設(shè)計(jì)

在課程學(xué)習(xí)的最初兩周，我們將介紹高質(zhì)量軟件所應(yīng)具備的性質(zhì)、影響可靠系統(tǒng)開(kāi)發(fā)的因素、導(dǎo)致軟件危機(jī)的原因，以及討論形式化方法的出現(xiàn)和發(fā)展情況，然后對(duì)線性時(shí)序邏輯和集論進(jìn)行簡(jiǎn)要的復(fù)習(xí)。接下來(lái)以案例教學(xué)法講授TLA和TLA+的基本概念，包括變量、謂詞、行為、行為時(shí)序邏輯公式、TLA+語(yǔ)法以及活性和安全性及其表示方法。最后學(xué)習(xí)使用TLA+對(duì)系統(tǒng)及其性質(zhì)進(jìn)行建模，并初步了解驗(yàn)證工具TLA ToolBox。

（三）課程考核

課程的考核由兩部分組成：作業(yè)和期末考試，兩者分別占學(xué)生最終成績(jī)的30%和70%。作業(yè)根據(jù)目標(biāo)知識(shí)又可分為兩個(gè)：第一個(gè)針對(duì)基礎(chǔ)知識(shí)的復(fù)習(xí)，包括集論和邏輯。此次作業(yè)可以讓學(xué)生使用半形式化的方法描述兩個(gè)較為簡(jiǎn)單的系統(tǒng)。另一作業(yè)強(qiáng)調(diào)形式化描述，可讓學(xué)生使用TLA+描述一個(gè)稍微復(fù)雜一點(diǎn)的系統(tǒng)。

考核標(biāo)準(zhǔn)應(yīng)事先告知學(xué)生，這樣有利于學(xué)生集中精力學(xué)習(xí)描述系統(tǒng)的具體問(wèn)題，而不必糾結(jié)于與本課程目標(biāo)無(wú)關(guān)的、不必要的細(xì)節(jié)。這一標(biāo)準(zhǔn)必須以學(xué)生為本，并有利于學(xué)生理解給定系統(tǒng)狀態(tài)的形式化描述，并能以此為基礎(chǔ)給出系統(tǒng)運(yùn)行的形式化描述；理解系統(tǒng)可能約束條件，并將此約束形式化語(yǔ)言轉(zhuǎn)化成系統(tǒng)不變量； 學(xué)會(huì)編寫(xiě)結(jié)構(gòu)良好的TLA+描述程序，對(duì)系統(tǒng)進(jìn)行完整建模；構(gòu)建健壯的形式化描述；對(duì)他們?cè)赥LA+描述中使用的概念提供合理解釋。

另外，考試試卷的設(shè)計(jì)應(yīng)能夠反映學(xué)生對(duì)形式化描述的理解和構(gòu)建兩方面的能力。這些能力就是通過(guò)平時(shí)的練習(xí)獲得的，如前面提到的解釋和判斷給定的形式化描述、將非形式描述轉(zhuǎn)化為形式描述等。

通過(guò)一個(gè)學(xué)期的教學(xué)實(shí)踐及對(duì)學(xué)生的調(diào)查，我們提出的形式化方法課程教學(xué)目標(biāo)、教學(xué)方法和教學(xué)評(píng)價(jià)方法取得了良好效果。這不僅提高學(xué)生了的學(xué)習(xí)積極性，讓學(xué)生初步掌握了一種設(shè)計(jì)可靠軟件的重要方法，也培養(yǎng)了學(xué)生對(duì)其他課程也很有用的數(shù)學(xué)抽象技能，學(xué)生普遍反映良好。

［參考文獻(xiàn)］

［1］古天龍. 軟件開(kāi)發(fā)的形式化方法［M］. 北京:高等教育出版社，2005.

［2］古天龍,董榮勝.歐洲高校計(jì)算機(jī)專(zhuān)業(yè)形式化方法課程教學(xué)［J］.計(jì)算機(jī)教育,2008,（10）: 99-103.

［3］Lamport L. The Temporal Logic of Actions［J］. ACM Trans on Programming Languages and Systems, 2009, 16(3):872-923.

［4］Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers［M］. Addison-Wesley, July 2003.

［責(zé)任編輯：劉鳳華］