欧洲高等院校计算机学科形式化方法教育探析.pdf

中国大学教学 2007 年第 11 期 48古天龙，桂林电子科技大学副校长、教授，教育部高等学校计算机科学与技术教学指导委员会软件工程专业教学指导分委员会委员 欧洲高等院校计算机学科形式化方法教育探析 古天龙古天龙 摘 要：本文基于欧洲形式化方法协会教育研究分会 FME-SoE(Formal Methods Europe Association - Subgroup on Education)所发布的欧洲高等院校计算机学科本科生形式化方法教育的调查分析报告，对欧洲高等院校的形式化方法教育知识体系进行介绍，总结给出了形式化方法教育可能采取的三种模式以期对国内高校计算机学科相关专业开设形式化方法课程提供参考 关键词：计算机学科；形式化方法；知识体系；课程教学 一、引言 形式化方法是基于数学上的形式机制的计算机系统研究方法客观地讲，有数学的应用，就有形式化方法但是，从计算机学科角度来讲，一般认为形式化方法是始于 20 世纪 60 年代末的 Floyd、Hoare 和 Manna 等在计算机程序正确性证明方面的研究当时由于“软件危机”， 人们试图用数学方法证明计算机程序的正确性而发展出各种程序验证方法，但是受程序规模的限制，这些方法并未达到预期的应用效果。

从 20 世纪 80 年代末开始，在计算机硬件设计领域形式化方法工业应用取得的成果， 掀起了形式化方法的学术研究和工业应用的热潮学术界和工程界的研究人员开展了大量的工作，建立了许多较为成熟并进入应用的形式化方法相关理论、方法和技术 从广义来讲， 形式化方法是计算机应用系统 （软件、硬件、软件和硬件混合）设计、实现及维护的系统工程方法；狭义来讲，形式化方法是离散数学、数理逻辑、抽象代数等计算机学科基础理论和计算机应用系统开发的结合，是指导计算机应用系统的工程化开发的方法和技术 计算机学科是一个年轻的工程学科，缺乏工程化的方法和技术一直是计算机应用系统研究的困难，也是困扰计算机学科教育的重要问题之一例如，迄今为止，大量的计算机软件开发依然没有摆脱试凑和经验， 从而，导致“软件危机”，以致于许多人们产生了“计算机是一门艺术，而不是一门科学”的错觉和误解 从 20 世纪 90 年代开始，计算机学科中工程化方法和技术——即形式化方法——的教育引起了欧美计算机教育界的高度重视和关注欧洲的英国、德国、法国、意大利、荷兰、西班牙等国家的高校相继为研究生开设了形式化方法方面的课程，并推广至本科生教育在 20世纪 90 年代中期， 美国开展了形式化方法教育研究， 并在美国顶尖的 35 所大学的计算机学科实施了研究生和本科生的教育实践。

IEEE-CS 和 ACM 联合任务组于 2004 年 5 月提交了计算教程-软件工程分册 CCSE（Computing Curriculum- Software Engineering）最终报告，在该报告给出的软件工 程 教 育 知 识 体 系SEEK （ Software Engineering Education Knowledge）中，“软件工程的形式化方法”（Formal Methods in Software Engineering）被列为一门核心课程（序列号为 SE313）[1,2]CCSE 最终报告的推出对计算机学科相关专业的形式化方法教育产生了重要的影响[3] 欧洲形式化方法协会于 2001 年成立了专门的形式化方法教育研究分会 FME-SoE(Formal Methods Europe Association - Subgroup on Education)， 目的在于研究并提出高等院校本科生形式化方法教育的知识体系及课程内容该组织于 2004 年 11 月发布了对欧洲 11 个国家、58所高等院校中的 117 门形式化方法教育相关课程的调研报告[4,5] 本文旨在介绍欧洲高等院校在计算机学科形式化方法教育的现状，建立形式化方法教育的初步知识体系，探讨形式化方法教育实施的可能途径。

二、形式化方法知识体系 欧洲形式化方法协会教育研究分会对欧洲高等院校本科生的形式化方法教育进行了调查分析， 将形式化方法分划为 6 个知识领域和 15 个知识单元 49形式化方法 FM（Formal Method）知识体系中的 6个知识领域， 即： 基础 （Foundations） ， 形式化规格 （Formal specification paradigms） ， 正确性验证及演算 （Correctness, verification and calculation） ， 形 式 化 语 义 （ Formal semantics） ，可执行规格支持（Support for executable specification） ，其它（Other Topics） 6 个知识领域包括的 15 个知识子领域或者知识单元，这些知识单元包含的知识点如下： FM01： 形式化方法的集合理论/拓扑基础的知识点，包括离散数学（DMat，含 ZF 集合理论、函数、关系、图、 树等） 、 格和不动点演算 （FixP） 、 Scott 域理论 （ScTD）等； FM02：形式化方法的逻辑基础的知识点， 包括一阶逻辑（FOL） 、Hoare 逻辑（HL） 、λ演算（LamC） 、时态逻辑（TL） 、线性时态逻辑（LTL） 、计算树逻辑（CTL） 、行为（Actions）时态逻辑（TLA）等； FM03：形式化方法的类型理论基础的知识点，包括类型理论和类型系统（TT） 、多型（Polytypism）和泛型（PolyT, Genericity）等； FM04：形式化方法的代数基础的知识点， 包括代数结构（AlS） 、程序构造数学（MPC，含范畴论）等； FM05：面向性质规格的知识点， 包括抽象数据类型（ADT） 、代数规格语言（CASL）等； FM06：面向模型规格的知识点， 包括抽象状态机器（ASM） 、形式化程序技术 （FPT，含前/后条件、不变量、证明、验证） 、B 方法（B） 、VDM、VDM 标准语言（VDML） 、VDM++（VPP） 、RAISE 规格语言（RSL） 、爱尔兰 VDAM（IVDM） 、Z、面向对象 Z（OZ） 、Alloy等； FM07： 多范式规格的知识点， 包括集成概念 （MPS，含多范式规格）等； FM08： 构造正确性的知识点， 包括程序代数 （AoP，含关系演算）等； FM09： 验证正确性的知识点， 包括程序验证 （PV） 、二叉决策图（BDD）等； FM10：机器检验正确性的知识点，包括模型检验（MC） 、自动定理证明（ATP） 、形式化方法测试（TFM）等； FM11：求精技术的知识点，包括算法求精（含循环不变量） （ARef） 、数据求精（DRef） 、求精演算（RC） 、B 求精（RefB）等； FM12： 程序语言语义的知识点， 包括行为 （Actions）语义（AS） 、代数语义（ASe） 、指称和操作语义（FS） 、抽象解释等（AbsI） ； FM13：形式化分布式、并发、移动的知识点，包括进程代数（PA） 、通信系统演算（CCS） 、通信顺序过程（CSP） 、π演算（PiC） 、Petri 网（Petri） 、有限状态进程（FSP） 、消息顺序图（MSC） 、LOTOS、增强 LOTOS（ELOT） 、Estelle、Unity、系统描述语言（SDL）等； FM14：声明式程序设计的知识点，包括函数式程序设计（FP） 、Haskell、标准 ML 语言（SML） 、扩展 ML语言（EML） 、CAML 语言（CAML） 、面向对象 CAML（Ocaml） 、Prolog 等； FM15：其它知识点，包括算法及复杂性（AL） 、软件体系结构（SA） 、Java 建模语言（JML） 、安全性分析技术（Safety）等。

三、总结 1． 形式化方法的工业应用需求和教学过程实践的经验积累，已越来越体现出形式化方法教育的必要性和可行性但是，国内计算机学科相关专业的形式化方法教育还相对薄弱，尚未在高等院校得到有效推广和实施目前，国内形式化方法教育面临如下几个方面的困难： （1）应用环境缺乏软件工程是形式化方法的主要工业应用领域国内软件企业近些年有很大的发展，但相当一部分企业仍然停留在个人英雄时代，很少需要团队合作或者是不需要大规模的合作所以形式化方法在这里无法真正得到推广，结果一些大的企业也只有从国外引进人才或者引进人才后再进行培训 （2）课程教材稀缺目前国内仅有数种形式化方法相关教材，且基本上都是针对某种表示或方法，如 Z、B、Petri 网等涉及形式化方法的软件工程、硬件设计方面的教材/专著也不过两三种 这些极大地制约了教师对形式化方法的全面了解和把握 （3）支撑工具匮乏在形式化方法的教育中，为了提高学生学习的兴趣和课程教学的效果，形式化方法支撑工具是必不可少的，但我们却很难发现有价值的支撑工具主要原因在于这些工具从认识到使用都需要花费很大的精力，当然开发相应的教学支撑工具也是需要花费较大的精力 （4）实验环境缺少。

形式化方法对于大规模应用系统开发尤为重要，教学单位一般只能提供小规模的教学实验环境，远远不及现实中的大规模系统学生又缺乏到大型企业中实践和实习的机会，不能很好地使学生对形式化有一个感性的认识 2． 形式化方法教育得到欧美国家高等院校的重视和大力推广不过近十余年的时间，建立完善的知识体系和课程教学内容还需要进一步的努力 从欧洲 58 所高校的课程开设情况，结合 CC2005 以及计算学科的特点，可50以看出形式化方法教育可能采取的途径为：专门语言/方法教学、综合内容课程教学、分散知识点教学 （1）专门语言/方法教学： 仅仅围绕一些特殊或专门的形式化方法/语言进行教学， 例如， Z 语言、 B 方法、VDM 语言、Petri 网、逻辑及程序证明等此方法可以对低年级学生实施教学，课程教学的目的在于培养学生能将形式化方法知识融会到其它后续课程的学习中，并逐步锻炼学生在计算机软、硬件系统的开发活动中使用形式化方法的能力不足之处在于教学计划中仅仅包含了单一的方法/语言， 学生不可能对形式化方法有广泛的认识和全面的了解同时，由于商业软件所采用形式化方法的多样性， 很难保证接受教育的学生达到学以致用，教学与实践的偏差难免太大。

（2）综合内容课程教学：围绕某一个主题或知识单元，开展多种形式化方法/语言的教学例如：软件开发中的形式化方法、形式化规格、程序验证技术、协议工程等此模式的优点在于不会使学生陷入仅仅学习几种形式化方法的思维中，同时也能很好地使学生从众多的方法中筛选对自己有用的方法并运用到实际的计算机软、硬件系统开发中去但是，由于课程内容覆盖面广，方法的基本理论和基本原理的深度不够，学生仅仅掌握和了解的是方法的一些符号和粗浅的技术这样，容易使学生产生误解，认为形式化方法仅仅是认识事物的一种符号表示方法，难以把形式化方法与计算机软、硬件系统的实际开发过程联系起来 （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] The Joint ACM/IEEE-C。