首先，这只能在没有副作用的算法上实现吗？
其次，我在哪里可以了解这个过程，有什么好书、文章等？
【问题讨论】：
标签： algorithm math proof correctness formal-verification
COQ 是产生正确 ocaml 输出的证明助手。不过这很复杂。我从来没有看它，但我的同事开始使用它，然后在两个月后停止使用它。这主要是因为他想更快地完成工作，但如果您需要验证算法，这可能是个好主意。
Here is a course 使用 COQ 并谈论证明算法。
还有here is a tutorial关于用COQ写学术论文。
【讨论】：
【讨论】：
我认为验证算法的正确性就是验证它是否符合规范。有一个名为Formal Methods 的理论计算机科学分支，如果您需要尽可能接近证明，这可能就是您正在寻找的东西。来自维基百科，
形式方法是一种特殊的方法 基于数学的技术 规范、开发和 软件和硬件的验证 系统
您将能够从链接的 Wikipedia 页面上的大量链接和 Formal Methods wiki 中找到许多学习资源和工具。
【讨论】：
通常正确性证明是针对手头的算法的。
但是，有几个众所周知的技巧可以重复使用。例如，对于递归算法，您可以使用loop invariants。
另一个常见的技巧是将原始问题简化为您的算法的正确性证明更容易显示的问题，然后将更简单的问题推广或证明可以将更简单的问题转化为原始问题的解决方案。 Here 是一个描述。
如果您有一个特定的算法，您可能会更好地询问如何为该算法构建证明而不是一般性答案。
【讨论】：
购买这些书：http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
Gries 的书，科学编程是很棒的东西。耐心、彻底、完整。
【讨论】：
Huth 和 Ryan 合着的《计算机科学中的逻辑》对用于验证系统的现代系统进行了合理易读的概述。曾几何时，人们谈论证明程序是正确的——使用可能有也可能没有副作用的编程语言。我从这本书和其他地方得到的印象是实际应用程序是不同的——例如证明协议是正确的，或者芯片的浮点单元可以正确划分，或者用于操作链表的无锁例程是正确的。
ACM 计算调查第 41 卷第 4 期（2009 年 10 月）是关于软件验证的特刊。通过搜索“Formal Methods: Practice and Experience”，您似乎可以在没有 ACM 帐户的情况下找到至少一篇论文。
【讨论】：
工具Frama-C（Elazar 建议在 cmets 中提供演示视频）为您提供了一种规范语言 ACSL，用于编写函数契约和各种分析器，以验证 C 函数是否满足其契约和安全属性，例如因为没有运行时错误。
扩展教程ACSL by example 显示了指定和验证的实际 C 算法的示例，并将无副作用函数与有效函数分开（无副作用函数被认为更容易并排在首位）教程）。该文档还很有趣，因为它不是由它所描述的工具的设计者编写的，因此它对这些技术提供了更新鲜和更具指导性的看法。
【讨论】：
如果您熟悉 LISP，那么您绝对应该查看 ACL2：http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
【讨论】：
Dijkstra 的编程学科 和他的 EWD 为形式验证作为编程科学奠定了基础。一个更简单的工作是 Wirth 的 系统编程，它从使用验证的简单方法开始。 Wirth 使用 pre-ISO Pascal 作为语言； Dijkstra 使用了一种类似于 Algol-68 的形式，称为 Guarded (GCL)。自 Dijkstra 和 Hoare 以来，形式验证已经成熟，但这些旧文本可能仍然是一个很好的起点。
【讨论】：
斯坦福大学的人开发的 PVS 工具是一个规范和验证系统。我研究了它，发现它对 Theoram Proving 非常有用。
【讨论】：
WRT (1)，您可能必须创建一个算法模型，以便在一个程序变量中“捕获”算法的副作用，以便对此类基于状态的副作用进行建模。
【讨论】：