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

李均濤

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

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

［中圖分類號］G423［文獻標識碼］A［文章編號］2095-3437（2012）02-0073-02

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

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

一、課程目標

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

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

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

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

第一，糾正學(xué)生“系統(tǒng)開發(fā)就是編寫代碼”的錯誤認識，明確形式化描述在精確刻畫系統(tǒng)和可靠系統(tǒng)開發(fā)中的重要意義。第二，理解可靠系統(tǒng)的開發(fā)過程。形式化描述可以通過發(fā)現(xiàn)不一致性和歧義性，為更好地理解可靠系統(tǒng)發(fā)揮重要作用。第三，認識在系統(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)細節(jié)的具體實現(xiàn)。在教學(xué)中，學(xué)生將學(xué)會如何對現(xiàn)實系統(tǒng)進行數(shù)學(xué)抽象。

二、描述語言的選擇

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

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

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

之所以選取TLA+作為描述語言，主要基于以下幾個方面的考慮：第一，TLA+已經(jīng)成為一個應(yīng)用較為普遍的形式化描述語言，不僅在學(xué)術(shù)界，而且目前在工業(yè)生產(chǎn)中也有了相當普遍的應(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é)機構(gòu)化和面向?qū)ο蟮姆椒ǎ@對學(xué)生鞏固以前的程序設(shè)計課程也是一個不小的幫助；第五，TLA+還具備一個正在不斷完善的集成開發(fā)環(huán)境TLA ToolBox，可以對建立的模型進行檢測和驗證，為學(xué)生理解和進一步學(xué)習(xí)形式化驗證打下基礎(chǔ)。

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

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

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

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

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

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

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

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

3.分組競賽

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

4.反向思考

在輔導(dǎo)課上給出一些TLA+描述的系統(tǒng)，要求學(xué)生用自然語言對其進行理解和解釋。這種方法可以讓學(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)致軟件危機的原因，以及討論形式化方法的出現(xiàn)和發(fā)展情況，然后對線性時序邏輯和集論進行簡要的復(fù)習(xí)。接下來以案例教學(xué)法講授TLA和TLA+的基本概念，包括變量、謂詞、行為、行為時序邏輯公式、TLA+語法以及活性和安全性及其表示方法。最后學(xué)習(xí)使用TLA+對系統(tǒng)及其性質(zhì)進行建模，并初步了解驗證工具TLA ToolBox。

（三）課程考核

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

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

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

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

［參考文獻］

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

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

［責任編輯：劉鳳華］