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

编

者

按

推进课程思政建设，是坚持社会主义办学方向、落实立德树人根本任务的重要举措，并与清华大学价值塑造、能力培养、知识传授“三位一体”的教育理念高度契合。然而，课程思政不是简单的“课程”加“思政”，而是课程当中有机地融入价值塑造的元素，努力实现二者的水乳交融，做到“如盐化水”、润物无声。

长期以来，我校教师围绕“三位一体”开展了卓有成效的教学实践，涌现出许多创新性的教学成果。为此，清华大学教务处特别推出“同行锦囊”3分钟音频课，陆续分享各类课程开展“课程思政”工作的具体经验与做法，力求“劳模可复制”，引领“同向”与“同行”。

基础课中的立德树人

贺飞：架起程序语言和形式逻辑之间的桥梁

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

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

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

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