高校计算机专业形式化方法课程教学研究

李均涛

［摘要］高校计算机专业开设形式化方法课程十分必要。必须设计课程目标和教学方法，并提出考核和评价学生学习效果的标准，通过严格的数学方法让学生获取对其他课程也很有益的知识、技术和能力。

［关键词］形式化方法课程教学行为时序逻辑系统描述

［中图分类号］G423［文献标识码］A［文章编号］2095-3437（2012）02-0073-02

软件的可靠性是人们最为关注的一个性质，尤其是对那些安全攸关的系统。为了使开发的软件系统更加可靠和安全，形式化方法应运而生且前景广阔，也越来越引起计算机科学界的关注。[1]在此背景下，许多科学协会如国际计算机协会、电子与电气工程师协会以及英国计算机协会都将形式化方法列为计算机科学本科教育的应开课程之一。[2]

本文将探讨形式化方法课程在计算机科学本科教学中的双重作用。此课程对计算机专业的本科生来说，不仅可以增长知识，更重要的是，可以提高学生更精准地描述事物的能力和技巧。

一、课程目标

形式化方法指的是各种数学建模技术，主要用于计算机系统行为的描述、建模，验证所设计的系统功能是否满足设计需求和安全性。这些描述和验证可以按照不同的精确度来进行。

形式化描述就是使用源自形式逻辑的标记方法来刻画需要建模的实际系统，包括系统的功能和这些功能的实现。

目前，欧美很多传统大学的计算机系开设了形式化方法课程，我国本科院校的计算机专业也已经开始跟进。这些课程大部分包含了形式化描述和形式化验证两部分，一般也会包含一个宽度优先搜索方法的内容。然而在形式化方法课程中，安排一种具体的形式化描述方法进行深入学习更为合适。主要原因如下：首先，计算机专业的本科生要理解数学和数学建模在计算机科学中的重要地位非常困难，要有一个渐进的过程。其次，形式化描述在某种程度上可以认为是程序设计的数学抽象，而学生在程序设计以及面向对象方法和系统设计分析等课程中，已经有了一定基础，学起来会更容易，且更有利于学生理解形式化描述在软件生命周期中的重要作用。最后，在学完本门课程后，学生可以基本掌握一种形式化描述的工具和方法，有助于学生对形式化方法的深入理解。

在这样的定位下，本课程的目标可以总结为：

第一，纠正学生“系统开发就是编写代码”的错误认识，明确形式化描述在精确刻画系统和可靠系统开发中的重要意义。第二，理解可靠系统的开发过程。形式化描述可以通过发现不一致性和歧义性，为更好地理解可靠系统发挥重要作用。第三，认识在系统开发的初期发现不一致性对于系统开发的重要性。第四，掌握一种形式化建模语言，可以为系统设计完整的、结构良好的数学模型。本文将以行为时序逻辑及其描述语言TLA+为例。[3]第五，培养学生的抽象能力。形式化描述实际上就是对现实系统或将要设计系统的一种数学抽象，它可以不关心系统细节的具体实现。在教学中，学生将学会如何对现实系统进行数学抽象。

二、描述语言的选择

对本门课程的设计，不能只是简单地教授描述语言的使用，更重要的是要让学生学会如何进行数学建模，包括如何进行抽象和解决问题。我们选择了TLA+作为载体，因为它更有助于实现我们的目标。

TLA是由美国科学家兰帕德（Leslie Lamport）提出的一种用来规约和推理并发系统的逻辑。它基于线性时序逻辑（LTL），通过对行为及各种操作符的扩展定义，可实现对并发系统及其性质的描述与验证。它最突出的特点是：系统及其性质可同时使用TLA公式来描述。基于TLA的描述语言TLA+以及模型检测工具箱TLA ToolBox已经成为独具特色的形式化验证工具。

TLA+整合了线性时序逻辑、行为时序逻辑以及部分集论的内容，是一种表达能力很强的形式化描述语言，并且非常简洁，很多庞大而又复杂的系统仅需一两页代码即可完成建模。[4]

之所以选取TLA+作为描述语言，主要基于以下几个方面的考虑：第一，TLA+已经成为一个应用较为普遍的形式化描述语言，不仅在学术界，而且目前在工业生产中也有了相当普遍的应用；第二，学生在之前已经学习了逻辑和集论的数学概念，这些概念是学习TLA+的基础；第三，学习TLA+可以让学生掌握对现实系统的过程抽象和数据抽象方法，使得学生能从实际系统的运行和具体数据的表示中抽离出来，更关注系统的整体框架，掌握抽象的步骤和方法；第四，TLA+使用了结机构化和面向对象的方法，这对学生巩固以前的程序设计课程也是一个不小的帮助；第五，TLA+还具备一个正在不断完善的集成开发环境TLA ToolBox，可以对建立的模型进行检测和验证，为学生理解和进一步学习形式化验证打下基础。

三、教学和评价方法

作为专业限选课，我们将本课程安排在大学三年级第一学期，总课时数为36学时，包括课堂教学和辅导。

（一）教学方法设计

为了实现课程教学目标，增强学生推理和解决问题的技巧和能力，我们采用以下教学方法：

1.主动学习

班级人数控制在40人以内，保持一个较低的师生比，有利于形成主动学习的氛围。

2.启发式教学

每当开始学习一个新的知识点，先介绍有关概念，然后利用一个实例来说明如何使用TLA+进行描述。当然，对实例的描述并不是通过教师的讲解来完成，而是由教师提出关键的、有启发作用的问题，然后引导学生自己写出形式描述语句。这样学生就可以积极地参与到形式化描述的过程中，而不是被动地接受信息，这样效果会更好。

3.分组竞赛

将班级学生随机分成由3～4人组成的学习小组，分别完成不同的案例。这些案例用自然语言给出，且故意包含一些模棱两可的词语，让学生在编写形式化描述时去发现。然后每个小组推举一人与教师进行讨论，让学生明白形式化描述与自然语言描述的区别及其重要性。最后由教师对完成情况进行点评，活跃课堂气氛，提高学生的学习积极性。

4.反向思考

在辅导课上给出一些TLA+描述的系统，要求学生用自然语言对其进行理解和解释。这种方法可以让学生了解一个好的软件开发者不仅要会设计程序，也必须会阅读和理解系统描述。

5.注重全局

本课程从一开始就引导学生使用TLA+建立系统架构的形式模型，其中包括如何阅读自然语言描述的系统需求，定义各种系统行为和性质，以及用行为和性质构建系统模型的时序逻辑公式。这种方法有助于学生建立良好的大局观，对今后设计系统的总体框架打下坚实的基础。

（二）课程内容设计

在课程学习的最初两周，我们将介绍高质量软件所应具备的性质、影响可靠系统开发的因素、导致软件危机的原因，以及讨论形式化方法的出现和发展情况，然后对线性时序逻辑和集论进行简要的复习。接下来以案例教学法讲授TLA和TLA+的基本概念，包括变量、谓词、行为、行为时序逻辑公式、TLA+语法以及活性和安全性及其表示方法。最后学习使用TLA+对系统及其性质进行建模，并初步了解验证工具TLA ToolBox。

（三）课程考核

课程的考核由两部分组成：作业和期末考试，两者分别占学生最终成绩的30%和70%。作业根据目标知识又可分为两个：第一个针对基础知识的复习，包括集论和逻辑。此次作业可以让学生使用半形式化的方法描述两个较为简单的系统。另一作业强调形式化描述，可让学生使用TLA+描述一个稍微复杂一点的系统。

考核标准应事先告知学生，这样有利于学生集中精力学习描述系统的具体问题，而不必纠结于与本课程目标无关的、不必要的细节。这一标准必须以学生为本，并有利于学生理解给定系统状态的形式化描述，并能以此为基础给出系统运行的形式化描述；理解系统可能约束条件，并将此约束形式化语言转化成系统不变量； 学会编写结构良好的TLA+描述程序，对系统进行完整建模；构建健壮的形式化描述；对他们在TLA+描述中使用的概念提供合理解释。

另外，考试试卷的设计应能够反映学生对形式化描述的理解和构建两方面的能力。这些能力就是通过平时的练习获得的，如前面提到的解释和判断给定的形式化描述、将非形式描述转化为形式描述等。

通过一个学期的教学实践及对学生的调查，我们提出的形式化方法课程教学目标、教学方法和教学评价方法取得了良好效果。这不仅提高学生了的学习积极性，让学生初步掌握了一种设计可靠软件的重要方法，也培养了学生对其他课程也很有用的数学抽象技能，学生普遍反映良好。

［参考文献］

［1］古天龙. 软件开发的形式化方法［M］. 北京:高等教育出版社，2005.

［2］古天龙,董荣胜.欧洲高校计算机专业形式化方法课程教学［J］.计算机教育,2008,（10）: 99-103.

［3］Lamport L. The Temporal Logic of Actions［J］. ACM Trans on Programming Languages and Systems, 2009, 16(3):872-923.

［4］Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers［M］. Addison-Wesley, July 2003.

［责任编辑：刘凤华］