程序设计方法学

101031 程序设计方法学

一、总述

1. 课堂

以电子课件为主，名义上的教材（老师会发电子版，估计你不会看）是：

《新编程序设计方法学》 陈海波，王申康编著 浙江大学出版社

主要教学内容为：

• 程序规范描述语言：断言
• 正规程序、基本程序、结构化定理
• 最弱前置谓词和程序语言的语义
• 结构化程序设计的基本原则和方法
• 程序正确性证明：不变式断言法、良序集方法、Hoare公理学方法
• 递归程序的正确性证明
• 程序变换技术（递归与循环的转换）
• Z 语言

对这方面感兴趣的同学可以阅读 https://softwarefoundations.cis.upenn.edu/

2. 作业

作业分为四次简单的小作业和期末报告，主要是证明，比较轻松。

期末项目任务是排序算法程序的正确性证明：

• 选择以下排序算法之一（对一数组按升序排列）：
• 选择排序（可用递归算法）
• 冒泡排序（可用递归算法）
• 插入排序（可用递归算法）
• 快速排序（用递归算法）
• 归并排序（用递归算法）

• 堆排序（用递归算法）

• 并选择以下程序正确性证明方法之一：

• Floyd 的不变式断言法（部分正确性）
• Floyd的良序集方法（程序终止性）
• Hoare的公理化方法（正向或反向证明）
• Dijkstra的弱谓词转换方法（完全正确性）
• 递归程序的良序归纳法（完全正确性）

要求： * 写出问题描述和程序规范，编写排序算法的程序（伪代码形式） * 画出结构化程序的流程图 * 写出完整的证明过程

3. 成绩

平时成绩（小作业）占 40 %，期末项目占 60 %。

期末项目有答辩环节。 老师称是否答辩与成绩无关，但是有助于老师评判。

老师给分一般、标准不明，会在群内公布优秀名单。这里给出一组数据，请自行分析。2023春季学期选课约 10 人，有 2 人选择答辩，仅给了 2 个优（但都不是答辩的同学）。

本课程没有旁听的必要，仅适合水良。

二、任课教师

1. 98715 Wang

上课信息密度较低，老师似乎计算机各方面都懂一点。在本课程方面，基本上能够完成PPT的讲授。比较友善，具有沟通能力。