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

摘要：ACM和IEEE-CS聯(lián)合任務(wù)組提交的計(jì)算教程CC2005，對(duì)計(jì)算機(jī)學(xué)科相關(guān)專業(yè)的教學(xué)產(chǎn)生了重大的影響。本文對(duì)計(jì)算教程CC2005中相關(guān)專業(yè)的知識(shí)體系進(jìn)行了分析，討論了形式化方法的相關(guān)課程計(jì)劃和教學(xué)內(nèi)容，以期對(duì)國(guó)內(nèi)高校開設(shè)形式化方法相關(guān)課程提供參考。

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

中圖分類號(hào)：G642文獻(xiàn)標(biāo)識(shí)碼：B

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

形式化方法是基于嚴(yán)密的、數(shù)學(xué)上的形式機(jī)制的計(jì)算機(jī)系統(tǒng)研究方法。ACM和IEEE-CS聯(lián)合任務(wù)組提交的計(jì)算教程CC2005的軟件工程分冊(cè)SE2004將“軟件工程的形式化方法(Formal Methods in Software Engineering)”列為一門核心課程 [3]。歐洲形式化方法學(xué)會(huì)于2001年成立了專門的形式化方法教育研究分會(huì)FME-SoE(Formal Methods Europe Association - Subgroup on Education)，并于2004年11月發(fā)布了對(duì)歐洲11個(gè)國(guó)家、58所高等院校形式化方法教育課程的調(diào)研報(bào)告[4，5]。這些工作為推進(jìn)計(jì)算機(jī)學(xué)科相關(guān)專業(yè)的形式化方法教育產(chǎn)生了積極的作用。

1CC2005簡(jiǎn)介

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

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

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

CC2005中的各個(gè)教程給出了相關(guān)專業(yè)的三級(jí)結(jié)構(gòu)知識(shí)體系：知識(shí)領(lǐng)域reg;知識(shí)單元reg;知識(shí)點(diǎn)；將知識(shí)單元中所對(duì)應(yīng)專業(yè)學(xué)生所必須了解和掌握的基本部分鑒別為核心單元，其余知識(shí)單元?jiǎng)t作為選修單元；根據(jù)知識(shí)單元中的知識(shí)點(diǎn)，規(guī)定實(shí)施知識(shí)單元所需的教學(xué)課時(shí)；依據(jù)核心單元及其教學(xué)課時(shí)，結(jié)合學(xué)生的培養(yǎng)方向，制訂出了相關(guān)專業(yè)學(xué)生的課程設(shè)置計(jì)劃和教學(xué)大綱。

2形式化方法相關(guān)知識(shí)內(nèi)容

計(jì)算機(jī)科學(xué)專業(yè)知識(shí)體系包括14個(gè)知識(shí)領(lǐng)域、132個(gè)知識(shí)單元，其中64個(gè)規(guī)定為核心單元。信息系統(tǒng)專業(yè)知識(shí)體系包括3個(gè)知識(shí)領(lǐng)域、29個(gè)知識(shí)單元。計(jì)算機(jī)工程專業(yè)知識(shí)體系包括18個(gè)知識(shí)領(lǐng)域、187個(gè)知識(shí)單元。軟件工程專業(yè)知識(shí)體系包括11個(gè)知識(shí)領(lǐng)域、58個(gè)知識(shí)單元。信息技術(shù)專業(yè)知識(shí)體系包括3個(gè)知識(shí)領(lǐng)域、29個(gè)知識(shí)單元。表1給出了各個(gè)專業(yè)知識(shí)體系中所包含的形式化方法相關(guān)知識(shí)點(diǎn)。

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

3結(jié)束語(yǔ)

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

參考文獻(xiàn)：

[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] 教育部高等學(xué)校計(jì)算機(jī)科學(xué)與技術(shù)教學(xué)指導(dǎo)委員會(huì). 高等學(xué)校計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)發(fā)展戰(zhàn)略研究報(bào)告暨專業(yè)規(guī)范(試行)[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ì)算機(jī)學(xué)科形式化方法教育探析[J]. 中國(guó)大學(xué)教學(xué)，2007，(11):48-50.