COMP6721 Formal Methods: The Lost Art
（非）形式化方法是一种实用的计算机程序编写和设计技术，使程序易于理解并在之后易于维护。它们只是“良好的编程实践”中的一部分，与该更大集合有所区别，因为对于我们考虑的方法，计算机科学界已经确定了这些结构背后的科学原理：我们知道它们为什么有效。
不同寻常的是，这门课程没有采用传统的教授科学理论，然后将其转变为实际的编程“思维工具”的方法。相反，我们首先教授思维工具，在实例中尝试它们，并一旦证明了它们的有效性，我们将深入了解它们的来源。
最初，课程内容将涉及常规程序，也就是必须“输出正确结果”的程序（即功能正确性，排序程序是一个简单的例子）。然后，我们将探讨更大规模的模块化技术及其思考方式；最后，我们将探索并发程序，即同时运行多个组件的程序。
本课程假设学生具备编写小型命令式程序的能力。它被设计为与COMP1511兼容；然而，其他初级编程课程应具备类似的技能要求。本课程主要使用“Python”编程语言。
学生应能够将计算机的更抽象、理论的一面应用到编写更好的程序中，而不必详细掌握理论本身。
学生应能够定义程序正确性断言和循环不变量，并在开发程序时使用静态推理。
学生应能够通过逐步精化和更改数据表示进行基于形式化的程序开发。
学生应看到并发性的复杂性，并学会一些控制并发性和关于并发性的推理技巧。