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

摘要：本文基于欧洲形式化方法协会教育研究分会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 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)、通信顺序过程

(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以及计算学科的特点，可以看出形式化方法教育可能采取的途径为：专门语言／方法教学、综合内容课程教学、分散知识点教学。

(1)专门语言／方法教学： 仅仅围绕一些特殊或专门的形式化方法／语言进行教学，例如，Z语言、B方法、VDM语言、Petri网、逻辑及程序证明等。此方法可以对低年级学生实施教学，课程教学的目的在于培养学生能将形式化方法知识融会到其它后续课程的学习中，并逐步锻炼学生在计算机软、硬件系统的开发活动中使用形式化方法的能力。不足之处在于教学计划中仅仅包含了单一的方法／语言，学生不可能对形式化方法有广泛的认识和全面的了解。同时，由于商业软件所采用形式化方法的多样性，很难保证接受教育的学生达到学以致用，教学与实践的偏差难免太大。

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

(3)分散知识点教学：将形式化方法的知识点融入到相关课程分散教学。例如在离散数学、数据结构、软件体系结构、软件工程、编译原理、人工智能、数字电路设计、计算机网络等课程中增加相关内容。优点在于把形式化方法贯穿在计算机学科的教学过程中，逐步渗透、循序渐进，培养学生的形式化方法思维能力和利用形式化方法实践计算机软／硬件系统开发的能力。这种模式的挑战在于需要大范围的修订计算机学科中各相关课程的教学内容，对授课教师也提出了更高的要求。