計算教程ＣＣ２００５中的形式化方法教育

摘要：ACM和IEEE-CS聯合任務組提交的計算教程CC2005，對計算機學科相關專業的教學產生了重大的影響。本文對計算教程CC2005中相關專業的知識體系進行了分析，討論了形式化方法的相關課程計劃和教學內容，以期對國內高校開設形式化方法相關課程提供參考。

關鍵詞：計算機學科；計算教程；CC2005；形式化方法；知識體系

中圖分類號：G642文獻標識碼：B

計算機科學技術日新月異、飛速發展，使得高等院校的計算機學科相關專業教育面臨嚴峻的挑戰。為了適應工業應用和大學教育的新形勢要求，確定合理的人才培養目標、知識體系及課程內容規范，美國計算機協會ACM和電子電氣工程師學會計算機分會IEEE-CS聯合制定并發布了計算教程CC 2005(Computing Curricula 2005)[1]。該報告的推出對全球計算學科相關專業的計算機教育產生了重要的影響，我國教育部高等學校計算機科學與技術教學指導委員會制訂了《高等學校計算機科學與技術專業發展戰略研究報告暨專業規范(試行)》[2]。

形式化方法是基于嚴密的、數學上的形式機制的計算機系統研究方法。ACM和IEEE-CS聯合任務組提交的計算教程CC2005的軟件工程分冊SE2004將“軟件工程的形式化方法(Formal Methods in Software Engineering)”列為一門核心課程 [3]。歐洲形式化方法學會于2001年成立了專門的形式化方法教育研究分會FME-SoE(Formal Methods Europe Association - Subgroup on Education)，并于2004年11月發布了對歐洲11個國家、58所高等院校形式化方法教育課程的調研報告[4，5]。這些工作為推進計算機學科相關專業的形式化方法教育產生了積極的作用。

1CC2005簡介

計算機技術及其工業革命對人類社會發展產生了深遠和重大的影響。從計算機誕生至今，計算學科的相關專業教育就引起了人們的極大關注。國際學術學會組織對于高等院校計算教程的制訂和規范一致給予了高度關注。ACM學會于1968年、1978年和1972年分別出版了計算機科學(CS：Computer Science)教程Curriculum’68、Curriculum’78和信息系統(IS：Information Systems)教程。IEEE-CS學會于1977年發布了計算機科學與工程教學計劃報告，并于1983年對其進行了修改完善。國際信息技術職業協會AITP(Association for Information Technology Professionals)于1985年發布了首部信息系統教程。ACM和IEEE-CS聯合任務組于1991年出版了著名的計算教程CC’91(Computing Curricula 1991)，給出了計算機科學和計算機工程(CE：Computer Engineering)專業四年制學士課程計劃。ACM于1993年發布了計算機科學、計算機工程、信息系統、計算機支持業務(computer support services)和其他領域計算共五個專業的二年制輔修學位教程。國際信息系統學會AIS(Association for Information Systems)和ACM、AITP于1997年公布了四年制信息系統專業學士學位教程。

計算教程CC’91對世界范圍的計算機教育產生了巨大的影響。但是，隨著計算機科學和技術的飛速發展，計算學科領域不僅在縱向上迅速發展，而且在橫向上急劇擴展，計算學科相關的各種不同課程也隨之迅猛增加。CC’91漸漸暴露出了各種局限性和不足。在1998年秋季，ACM和IEEE-CS再次合作，成立了聯合任務組旨在對CC’91進行修訂和完善，建立能為各種計算學科的學位課程設置提供指南的新教程。隨著工作的推進，任務組成員認識到：計算已經深入到如此多而廣的領域，以致從一門學科的單一角度來看問題是遠遠不夠的。各種計算學科領域內容的豐富程度和廣度要求以一種新的方式來定義和規范計算課程，該工作的完成需要ACM、IEEE-CS、AIS以及其它專業協會的合作。ACM和IEEE-CS聯合任務組于2001年12月發布了計算教程CC2001(Computing Curricula 2001)。CC2001報告包含了兩個方面重要內容：新的計算教程結構(稱為CC2001模型)；計算機科學本科生學位計劃的詳

細課程指南。由于CC2001報告包括了計算機科學課程指南，所以把那些涉及到計算機科學內容的部分當作計算科學教程CS2001。信息系統相關組織于2002年發布了信息系統更新報告信息系統教程IS2002。軟件工程教程分冊SE2004、計算機工程教程分冊CE2004、信息技術(IT：Information Technology)教程分冊IT2005分別于2004年8月、2004年12月、2005年10月完成。計算教程CC2005由計算教程概要報告CC2005、計算科學教程CC2001(CS2001)、信息系統教程IS2002、軟件工程教程SE2004、計算機工程教程CE2004、信息技術教程IT2005、其它教程(待增加)共7部分組成。概要報告CC2005對該版本教程所涉及專業計算機科學、信息系統、軟件工程、計算機工程、信息技術進行了全面的介紹，并給出了各個專業學位計劃規范制訂的指導性原則。各專業學位計劃的知識體系以及課程設置和內容在相應分冊中詳細闡述。

CC2005中的各個教程給出了相關專業的三級結構知識體系：知識領域reg;知識單元reg;知識點；將知識單元中所對應專業學生所必須了解和掌握的基本部分鑒別為核心單元，其余知識單元則作為選修單元；根據知識單元中的知識點，規定實施知識單元所需的教學課時；依據核心單元及其教學課時，結合學生的培養方向，制訂出了相關專業學生的課程設置計劃和教學大綱。

2形式化方法相關知識內容

計算機科學專業知識體系包括14個知識領域、132個知識單元，其中64個規定為核心單元。信息系統專業知識體系包括3個知識領域、29個知識單元。計算機工程專業知識體系包括18個知識領域、187個知識單元。軟件工程專業知識體系包括11個知識領域、58個知識單元。信息技術專業知識體系包括3個知識領域、29個知識單元。表1給出了各個專業知識體系中所包含的形式化方法相關知識點。

計算教程CC2005中的個專業分冊，給出了相關專業的課程設置和教學內容建議。這些課程中的一些涉及到了形式化方法知識的教學，表2列出了相關課程設置情況。值得一提的是，軟件工程教程SE2004中，將形式化方法單獨設置為一門獨立的核心課程—軟件工程的形式化方法(Formal Methods in Software Engineering)(SE313)。

3結束語

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

參考文獻：

[1] The Joint ACM/IEEE-CS Task Force on Computing Curricula. Computing curricula 2005 – the Overview Report[R]. ACM and IEEE Computer Society，2005.

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

[3] The Joint ACM/IEEE-CS Task Force on Computing Curricula. Software Engineering 2004[R]. ACM and IEEE Computer Society，2004.

[4] FME Subgroup on Education. A survey of formal methods courses in European higher education[C]. LNCS 3294: Teaching Formal Methods，2004:235-248.

[5] 古天龍. 歐洲高等院校計算機學科形式化方法教育探析[J]. 中國大學教學，2007，(11):48-50.