基础课中的立德树人 | 软件学院贺飞：架起程序语言和形式逻辑之间的桥梁

大家好，我是软件学院的贺飞，我承担的是本科生的“软件分析与验证”课程，以下是我的同行锦囊。

软件工程教学中存在基础课程与应用课程衔接不够紧密的问题。一方面，同学们在学完数理逻辑等基础课程之后常常不知道其具体的用途。另一方面，同学们学了很多编程语言，却不一定知道这些程序语言背后的原理是什么。我开设这门课程，希望能够帮助大家建立起程序和逻辑之间的深刻联系，加深对程序的深层次理解。

为此，我精心设计了课程教学内容，共三部分。第一部分是形式逻辑。同学们在“离散数学”课程中已经学习过基本的一阶逻辑系统。对于刻画程序语义，一阶逻辑的表达能力已经足够，但是其可计算性不强。因此我们需要根据程序特点对一阶逻辑进行合理的限制，得到可判定的、带背景理论的一阶逻辑。第二部分内容是判定过程，主要讨论可判定逻辑系统的判定算法，即逻辑系统的计算问题。第三部分内容是程序语言，着重介绍如何基于形式逻辑来理解程序的行为和语义。通过上述三部分内容，我们将逻辑、计算和程序贯连了起来。

通过本课程的学习，同学们对程序语言将会有更深刻的理解，能够利用形式逻辑等数学工具对程序进行抽象和推理，进而将具备编写更有效、更安全、更可靠软件代码的能力。