UQ昆士兰大学CSSE7100程序推理课程介绍

课程代码：CSSE7100

课程名称：程序推理Reasoning about Programs

所属学院：信息技术与电气工程学院

课程级别：本科生

先决条件：MATH7861和CSSE7023

课程描述：

编写软件的目的是为了完成一项期望的任务。编写这样的软件需要算法问题解决技巧；要正确地做到这一点，需要我们精确地完成手头的任务，并且能够推断出一个实现满足了任务的精确需求。

这门关于编程的高级课程介绍了结构化的、正式的方法，用于:指定程序的期望行为，显示程序相对于它们的规范是正确的，以及从规范中导出算法。这些技术旨在帮助开发人员解决编程问题，并生产高质量的软件。

学习目标：

1、解释程序的正式规范和验证的基本原理。

2、以数学上精确的方式指定程序中方法和函数的期望行为。

3、使用正式的技术来验证一个方法相对于它的规范是正确的。

4、使用正式的结构化方法，从抽象规范中获得正确的方法。

5、指定并验证程序中对象和数据结构的正确性。

6、使用一个验证工具来自动和交互地验证程序的正确性。