| 教学周次 | 日期 | 教学内容 | 作业 |
|---|---|---|---|
| 1 | 2024-2-27 |
软件工程建模与形式化方法介绍 讲义：教学大纲实施细则, KL教学平台使用手册 |
|
| 2 | 2024-3-5 | 函数式程序设计1：Haskell语言简介，环境配置，基本语法，函数，高阶函数，枚举类型 | |
| 3 | 2024-3-12 | 函数式程序设计2：递归，类型类，多态，函数式数据结构 | |
| 4 | 2024-3-19 | 函数式程序设计3：Functor，Applicative functors，Monad，IO | 作业1 |
| 5 | 2024-3-26 | 逻辑基础1：简介，基本语法，使用Coq对程序建模 | |
| 6 | 2024-4-2 | 逻辑基础2：命题逻辑 | |
| 7 | 2024-4-9 | 逻辑基础3：谓词逻辑 | |
| 8 | 2024-4-16 | 逻辑基础4：数学归纳法，关系 | 作业1截止，作业2 |
| 9 | 2024-4-23 | 逻辑基础5：Coq中的数据结构，程序提取，类型论与科里霍华德对应 | |
| 10 | 2024-4-30 | 指令式程序逻辑1：指令式程序逻辑简介，使用Coq建模指令式程序 | |
| 11 | 2024-5-7 | 指令式程序逻辑2：霍尔逻辑 | |
| 12 | 2024-5-14 | 指令式程序逻辑3：分离逻辑，Dafny简介 | 作业2截止，作业3 |
| 13 | 2024-5-21 | 高级主题：依赖类型论 | |
| 14 | 2024-5-28 | 案例1：CompCert | |
| 15 | 2024-6-4 | 案例2：FSCQ | |
| 16 | 2024-6-11 | 期末考试 | 作业3截止 |