教师:贺飞
助教:谢兴宇、韩志磊、徐荣琛、刘江宜
教师答疑时间:每周一下午15:00~17:00
教师答疑地点:东配楼11-307
助教答疑时间:每周四下午14:00~17:00
助教答疑地点:东配楼11-321
期末考试时间:2022-06-11(周六) 19:00~21:00 期末考试地点:建馆报告厅
课程教学计划如下(暂定,可能根据实际教学情况进行调整):
周次 | 日期 | 教学内容 | 作业 | 备注 |
---|---|---|---|---|
1 | 2022/02/21 | 绪论 | ||
2 | 2022/02/28 | 命题逻辑 | ||
3 | 2022/03/07 | 一阶逻辑 | Homework 1 (DDL:03/21) | |
4 | 2022/03/14 | 一阶理论 IMP程序语言及其语义 助教课:Z3工具(时间另行通知) |
||
5 | 2022/03/21 | 演绎程序验证 | Homework 2 (DDL:04/04) | |
6 | 2022/03/28 | 循环 | ||
7 | 2022/04/02 | 扩展IMP语言 | Homework 3 (DDL:04/18) | 清明调课 |
8 | 2022/04/11 | 验证条件 | ||
9 | 2022/04/18 | 扩展IMP语言 助教课:课程大作业说明 |
Homework 4 (DDL:05/09) | |
10 | 2022/04/25 | 程序终止性 | ||
11 | 2022/05/02 | 放假 | ||
12 | 2022/05/09 | 推导循环不变式 | ||
13 | 2022/05/16 | 程序的自动机表示 | ||
14 | 2022/05/23 | 自动程序验证(1) | Homework 5 (DDL:06/06) | |
15 | 2022/05/30 | 自动程序验证(2) | ||
16 | 2022/06/06 | 扩展性内容 |