首页 -> 2007年第11期
欧洲高等院校计算机学科形式化方法教育探析
作者：古天龙
关键词：计算机学科；形式化方法；知识体系；课程教学
一、引言
形式化方法是基于数学上的形式机制的计算机系统研究方法。客观地讲，有数学的应用，就有形式化方法。但是，从计算机学科角度来讲，一般认为形式化方法是始于20世纪60年代末的Floyd、Hoare和Manna等在计算机程序正确性证明方面的研究。当时由于“软件危机”，人们试图用数学方法证明计算机程序的正确性而发展出各种程序验证方法，但是受程序规模的限制，这些方法并未达到预期的应用效果。从20世纪80年代末开始，在计算机硬件设计领域形式化方法工业应用取得的成果，掀起了形式化方法的学术研究和工业应用的热潮。学术界和工程界的研究人员开展了大量的工作，建立了许多较为成熟并进入应用的形式化方法相关理论、方法和技术。从广义来讲，形式化方法是计算机应用系统(软件、硬件、软件和硬件混合)设计、实现及维护的系统工程方法；狭义来讲，形式化方法是离散数学、数理逻辑、抽象代数等计算机学科基础理论和计算机应用系统开发的结合，是指导计算机应用系统的工程化开发的方法和技术。
计算机学科是一个年轻的工程学科，缺乏工程化的方法和技术一直是计算机应用系统研究的困难，也是困扰计算机学科教育的重要问题之一。例如，迄今为止，大量的计算机软件开发依然没有摆脱试凑和经验，从而，导致“软件危机”，以致于许多人们产生了“计算机是一门艺术，而不是一门科学”的错觉和误解。
从20世纪90年代开始，计算机学科中工程化方法和技术——即形式化方法——的教育引起了欧美计算机教育界的高度重视和关注。欧洲的英国、德国、法国、意大利、荷兰、西班牙等国家的高校相继为研究生开设了形式化方法方面的课程，并推广至本科生教育。在20世纪90年代中期，美国开展了形式化方法教育研究，并在美国顶尖的35所大学的计算机学科实施了研究生和本科生的教育实践。
IEEE-CS和ACM联合任务组于2004年5月提交了计算教程，软件工程分册CCSE(Computing Curriculum，Software Engineering)最终报告，在该报告给出的软件工程教育知识体系SEEK(Software EngineeringEducation Knowledge)中，“软件工程的形式化方法”(Formal Methods in Software Engineering)被列为一门核心课程(序列号为SE313)。CCSE最终报告的推出对计算机学科相关专业的形式化方法教育产生了重要的影响。
欧洲形式化方法协会于2001年成立了专门的形式化方法教育研究分会FME-SoE(Formal Methods EuropeAssociation-Subgroup on Education)，目的在于研究并提出高等院校本科生形式化方法教育的知识体系及课程内容。该组织于2004年11月发布了对欧洲11个国家、58所高等院校中的117门形式化方法教育相关课程的调研报告。
本文旨在介绍欧洲高等院校在计算机学科形式化方法教育的现状，建立形式化方法教育的初步知识体系，探讨形式化方法教育实施的可能途径。
二、形式化方法知识体系
欧洲形式化方法协会教育研究分会对欧洲高等院校本科生的形式化方法教育进行了调查分析，将形式化方法分划为6个知识领域和15个知识单元。
形式化方法FM(Formal Method)知识体系中的6个知识领域，即：基础(Foundations)，形式化规格(Formalspecification paradigms)，正确性验证及演算(Correctness，verification and calculation)，形式化语义(Formalsemantics)，可执行规格支持(Support for executablespecification)，其它(Other Topics)。
6个知识领域包括的15个知识子领域或者知识单元，这些知识单元包含的知识点如下：
FM01：形式化方法的集合理论／拓扑基础的知识点，包括离散数学(DMat，含ZF集合理论、函数、关系、图、树等)、格和不动点演算(FixP)、ScoR域理论(ScTD)等；
FM02：形式化方法的逻辑基础的知识点，包括一阶逻辑(FOL)、Hoare逻辑(HL)、λ演算(LamC)、时态逻辑(TL)、线性时态逻辑(LTL)、计算树逻辑(CTL)、行为(Actions)时态逻辑(TLA)等；
FM03：形式化方法的类型理论基础的知识点，包括类型理论和类型系统(TT)、多型(Polytypism)和泛型(PolyT，Geneficity)等；
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)等；
FMIO：机器检验正确性的知识点，包括模型检验(MC)、自动定理证明(ATP)、形式化方法测试(TFM)等；
FM11：求精技术的知识点，包括算法求精(含循环不变量)(ARef)、数据求精(DRef)、求精演算(RC)、B求精(RefB)等；
FM12：程序语言语义的知识点，包括行为(Actions)语义(AS)、代数语义(ASe)、指称和操作语义(FS)、抽象解释等(Absl)；
FM13：形式化分布式、并发、移动的知识点，包括进程代数(PA)、通信系统演算(CCS)、通信顺序过程
[2]