李均濤

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

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

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

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

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

一、課程目標(biāo)

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

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

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

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

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

二、描述語言的選擇

對本門課程的設(shè)計，不能只是簡單地教授描述語言的使用，更重要的是要讓學(xué)生學(xué)會如何進(jìn)行數(shù)學(xué)建模，包括如何進(jìn)行抽象和解決問題。我們選擇了TLA+作為載體，因為它更有助于實現(xiàn)我們的目標(biāo)。

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

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

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

三、教學(xué)和評價方法

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

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

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

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

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

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

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

3.分組競賽

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

4.反向思考

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

5.注重全局

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

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

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

（三）課程考核

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

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

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

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

［參考文獻(xiàn)］

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

［2］古天龍,董榮勝.歐洲高校計算機(jī)專業(yè)形式化方法課程教學(xué)［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é)任編輯：劉鳳華］