CSSE7100/3100 Reasoning about Programs有关程序的推理

      CSSE7100/3100 Reasoning about Programs有关程序的推理

　　1.一般课程信息

　　UQ学生：请从Learn.UQ或mySI-net访问个人资料，以访问此个人资料中保存的所有课程参与者详细信息。

1.1课程详情

课程编号： CSSE7100

课程名称：关于程序的推理

协调单位：信息技术与电气工程学院

学期： 2024年第1学期

模式：内部

级别：研究生课程

地点：圣卢西亚

台数： 2

每周接触时间： 3C

先决条件： MATH7861和CSSE7023

课程说明：编写软件的目的是要执行所需的任务。编写此类软件需要算法问题解决能力;正确地做到这一点要求我们精确地处理手头的任务，并能够推断出实现满足任务的精确要求。这门编程高级课程介绍了结构化的形式化方法，这些方法用于：指定程序的期望行为，表明程序就其规范而言是正确的，并从规范中推导算法。这些技术旨在帮助开发人员解决编程问题并生产高质量的软件。

假设背景：

要求学生至少完成2门编程课程，并对谓词逻辑有扎实的理解。

1.2课程简介

本课程的主要目的是向您介绍一些技术和工具，使您可以对程序进行推理，以表明该程序符合所有有效输入的规范，而不仅仅是单个测试输入。换句话说，您将学习验证程序是否满足其规范。

在进入关于程序的推理时，您将学习基本的编程技术以及谓词逻辑的证明。该课程将这两部分学习结合在一起，以使用逻辑推理程序。您还将学习使用最先进的工具来自动化和检查程序正确性的证明。

总体而言，该课程可以看作是编程的高级课程，重点是提高您的能力，以确保您编写的程序满足其规范。

根据先前学生的反馈对课程进行更改

“ 我认为另一件事会很好，那就是以计算机语言实际完成的一些示例或练习，也许只是一些简单的程序，可以从规范中提取规范并进行验证，或者在从规范中派生出程序后编写。我理解这将需要学生熟悉特定的语言，但是每个学生都应该熟悉CSSE早期课程中的python或java，这样做将有助于弥合理论与实际应用之间的鸿沟。 ”

现在，该课程以Dafny编程语言为基础。Dafny起源于Microsoft Research，现在也正在Amazon Web Services中开发。它与基于C的语言(例如C#和Java)有很多共同点。

“ 我希望本课程有更多内容：例如，学习使用讲座中提供的一些工具来展示真实程序的正确性，讨论如何将正式方法应用于生产软件以及在何处应用正式方法，自动证明等。 。 “

现在，该课程将Dafny验证工具广泛用于自动和交互式推理。

“ 对于作业2，只有一个问题占20%的问题有点令人生畏-如果某人一开始就努力将诸如特定问题的说明之类的内容放在一起，那可能会花费很多课程费用-这样的话，如果价值20%的作业多于一个问题，那就更好了。 ”

“ 除主要问题外，第二个作业本可以有几个较小的问题。”

CSSE7100/3100 Reasoning about Programs有关程序的推理该课程现在有4个小作业，而不是2个大作业。学生的工作量与前几年相同，但分布更多，有更多的反馈机会。