文章編號(hào)：1672-5913(2008)10-0099-05

摘要：本文對(duì)歐洲高等院校的計(jì)算機(jī)相關(guān)專業(yè)形式化方法教育進(jìn)行了介紹，主要包括形式化方法課程的知識(shí)體系、形式化方法教育的課程及其內(nèi)容。

關(guān)鍵詞：計(jì)算機(jī)學(xué)科；形式化方法；知識(shí)體系；歐洲高校

中圖分類號(hào)：G642

文獻(xiàn)標(biāo)識(shí)碼：B

形式化方法是基于嚴(yán)密的、數(shù)學(xué)上的形式機(jī)制的計(jì)算機(jī)系統(tǒng)研究方法。從20世紀(jì)90年代開始，計(jì)算機(jī)學(xué)科相關(guān)專業(yè)的形式化方法的教育引起了歐美教育界的高度重視和關(guān)注。歐洲的英國、德國、法國、意大利、荷蘭、西班牙等國家的高校相繼為研究生開設(shè)了形式化方法方面的課程，并推廣至本科生教育。從20世紀(jì)90年代中期開始，美國高校也開展了形式化方法教育研究，并在美國頂尖的35所大學(xué)的計(jì)算機(jī)學(xué)科實(shí)施了研究生和本科生的教育實(shí)踐。

IEEE-CS和ACM聯(lián)合任務(wù)組于2005年9月提交了計(jì)算教程CC2005(Computing Curricula 2005)最終報(bào)告，該報(bào)告的軟件工程分冊CCSE(Computing Curriculum- Software Engineering 2004)將“軟件工程的形式化方法(Formal Methods in Software Engineering)”列為一門核心課程。CC2005最終報(bào)告的推出對(duì)計(jì)算機(jī)學(xué)科相關(guān)專業(yè)的形式化方法教育產(chǎn)生了重要的影響。

歐洲形式化方法協(xié)會(huì)于2001年成立了專門的形式化方法教育研究分會(huì)FME-SoE(Formal Methods Europe Association - Subgroup on Education)，目的在于研究并提出高等院校本科生形式化方法教育的知識(shí)體系及課程內(nèi)容。該組織于2004年11月發(fā)布了對(duì)歐洲11個(gè)國家、58所高等院校中的117門形式化方法教育相關(guān)課程的調(diào)研報(bào)告。

1形式化方法知識(shí)體系

FME-SoE組織對(duì)歐洲高等院校本科生的形式化方法教育進(jìn)行了調(diào)查分析，將形式化方法分劃為6個(gè)知識(shí)領(lǐng)域和15個(gè)知識(shí)單元。圖1給出了該分析過程中形式化方法的知識(shí)體系。

圖1 形式化方法知識(shí)體系

形式化方法(FM-Formal Method)知識(shí)體系中的6個(gè)知識(shí)領(lǐng)域?yàn)椋孩?基礎(chǔ)(Foundations)；② 形式化規(guī)格(Formal specification paradigms)；③ 正確性驗(yàn)證及演算(Correctness， verification and calculation)；④ 形式化語義(Formal semantics)；⑤ 可執(zhí)行規(guī)格支持(Support for executable specification)；⑥ 其他(Other Topics)。

6個(gè)知識(shí)領(lǐng)域包括15個(gè)知識(shí)子領(lǐng)域或者知識(shí)單元：FM01形式化方法的集合理論/拓?fù)浠A(chǔ)(Set-theoretic/topological foundations of Formal Methods)；FM02 形式化方法的邏輯基礎(chǔ)(Logical foundations of Formal Methods)；FM03 形式化方法的類型理論基礎(chǔ)(Type-theoretic foundations of Formal Methods)；FM04 形式化方法的代數(shù)基礎(chǔ)(Algebraic foundations of Formal Methods)；FM05 面向性質(zhì)規(guī)格(Property oriented specification)；FM06 面向模型規(guī)格(Model oriented specification)；FM07 多范式規(guī)格(Multi-paradigm specification)；FM08 構(gòu)造正確性(Correct by construction)；FM09 驗(yàn)證正確性(Correct by verification)；FM10 機(jī)器檢驗(yàn)正確性(Correct by machine checking)；FM11 求精技術(shù)(Refinement techniques)；FM12 程序語言語義(Programming language semantics)；FM13 形式化分布式、并發(fā)、移動(dòng)(Formalizing distribution， concurrency and mobility)；FM14 聲明式程序設(shè)計(jì)(Declarative programming)；FM15 其他。這些知識(shí)單元包含的知識(shí)點(diǎn)如表1所示。

2 形式化方法課程

形式化方法教育過程中，相關(guān)形式化方法工具的支持是非常重要和必要的。歐洲高等院校在形式化方法研究和教育過程中，開發(fā)了許多相關(guān)工具。形式化工具有：Actress、Alloy、AtelierB、B-Toolkit(Btlk)、BDDC、CADP、CADiZ、CASL、Coq、CommUnity、CWB、ESCJava、FDR、FuZZ、GHC、Gofer、Hugs、HOL、集成網(wǎng)絡(luò)分析器(INA)、Isabelle、IVDM、Lotrec、LTSA、NuSMV、Petri網(wǎng)程序設(shè)計(jì)環(huán)境(Petri)、PVS、PicT、RAISEtools、RAT、RML、SPIN、T-Logic、TRIO、UPAAL、VDMT、WHY、ZANS、ZEVES、ZTC等已在相關(guān)課程教學(xué)中得到使用。在這里，我們對(duì)已開設(shè)課程總結(jié)如表2所示。對(duì)這些課程進(jìn)行頻次統(tǒng)計(jì)分類分析，可以發(fā)現(xiàn)：知識(shí)單元FM06、FM02和FM13具有較高開課率，分別為52門、27門和27門；語言Z和B在教學(xué)中得到了較多介紹，分別為16門和15門；形式化方法工具SPIN和VDMT得到了較多使用，均為6門。

3 結(jié)語

形式化方法教育得到歐、美國家高等院校的重視和大力推廣不過是十余年的時(shí)間，建立完善的知識(shí)體系和課程教學(xué)內(nèi)容還需要進(jìn)一步的努力。從歐洲58所高校的課程開設(shè)情況來看，雖然形式化方法教育得到了大范圍的實(shí)施，但是課程內(nèi)容、授課教材、輔助工具等還比較散雜，建立形式化方法課程的知識(shí)內(nèi)容規(guī)范、編寫相關(guān)規(guī)范指導(dǎo)下的教材、開發(fā)相關(guān)規(guī)范指導(dǎo)下的輔助工具，是亟待解決的問題。

形式化方法的工業(yè)應(yīng)用需求和教學(xué)過程實(shí)踐的經(jīng)驗(yàn)積累，已愈來愈體現(xiàn)出計(jì)算機(jī)相關(guān)專業(yè)形式化方法教育的必要性和可行性。國內(nèi)計(jì)算相關(guān)專業(yè)的形式化方法教育還相當(dāng)薄弱，尚未在高等院校得到有效推廣和實(shí)施。計(jì)算機(jī)相關(guān)專業(yè)形式化方法課程教學(xué)的有效推進(jìn)還有賴于課程教材、實(shí)驗(yàn)環(huán)境、支撐工具以及應(yīng)用環(huán)境等方面的突破。

參考文獻(xiàn)

[1] 教育部高等學(xué)校計(jì)算機(jī)科學(xué)與技術(shù)教學(xué)指導(dǎo)委員會(huì). 高等學(xué)校計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)發(fā)展戰(zhàn)略研究報(bào)告暨專業(yè)規(guī)范(試行)[M]. 北京:高等教育出版社，2006.