歐洲高校計算機專業的形式化方法課程教學

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

摘要：本文對歐洲高等院校的計算機相關專業形式化方法教育進行了介紹，主要包括形式化方法課程的知識體系、形式化方法教育的課程及其內容。

關鍵詞：計算機學科；形式化方法；知識體系；歐洲高校

中圖分類號：G642

文獻標識碼：B

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

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

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

1形式化方法知識體系

FME-SoE組織對歐洲高等院校本科生的形式化方法教育進行了調查分析，將形式化方法分劃為6個知識領域和15個知識單元。圖1給出了該分析過程中形式化方法的知識體系。

圖1 形式化方法知識體系

形式化方法(FM-Formal Method)知識體系中的6個知識領域為：① 基礎(Foundations)；② 形式化規格(Formal specification paradigms)；③ 正確性驗證及演算(Correctness， verification and calculation)；④ 形式化語義(Formal semantics)；⑤ 可執行規格支持(Support for executable specification)；⑥ 其他(Other Topics)。

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

2 形式化方法課程

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

3 結語

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

形式化方法的工業應用需求和教學過程實踐的經驗積累，已愈來愈體現出計算機相關專業形式化方法教育的必要性和可行性。國內計算相關專業的形式化方法教育還相當薄弱，尚未在高等院校得到有效推廣和實施。計算機相關專業形式化方法課程教學的有效推進還有賴于課程教材、實驗環境、支撐工具以及應用環境等方面的突破。

參考文獻

[1] 教育部高等學校計算機科學與技術教學指導委員會. 高等學校計算機科學與技術專業發展戰略研究報告暨專業規范(試行)[M]. 北京:高等教育出版社，2006.