形式化验证算法的正确性
首先，这是否只能在没有副作用的算法上才有可能？
其次，我在哪里可以了解这个过程，有什么好的书籍、文章等？
First of all, is this only possible on algorithms which have no side effects?
Secondly, where could I learn about this process, any good books, articles, etc?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（11）
COQ 是一个证明助手，可以生成正确的 ocaml 输出。但它相当复杂。我从来没有抽出时间去看它，但我的同事开始使用它，两个月后就停止使用了。这主要是因为他想更快地完成工作，但如果您需要验证算法，这可能是一个好主意。
这里有一门课程，它使用 COQ 并讨论证明算法。
这里有一个关于在 COQ 中撰写学术论文的教程。
COQ is a proof assistant that produces correct ocaml output. It's pretty complicated though. I never got around to looking at it, but my coworker started and then stopped using it after two months. It was mostly because he wanted to get things done quicker, but if you need to verify an algorithm this might be a good idea.
Here is a course that uses COQ and talks about proving algorithms.
And here is a tutorial about writing academic papers in COQ.
我认为验证算法的正确性就是验证其与规范的一致性。理论计算机科学有一个分支，称为形式化方法，如果你需要尽可能接近证据。来自维基百科，
能够从链接的维基百科页面上的大量链接以及 正式方法维基。
I think that verifying the correctness of an algorithm would be validating its conformance with a specification. There is a branch of theoretical Computer Science called Formal Methods which may be what you are looking for if you need to get as close to proof as you can. From wikipedia,
You will be able to find many learning resources and tools from the multitude of links on the linked Wikipedia page and from the Formal Methods wiki.
通常正确性的证明是针对当前算法的。
然而，有一些众所周知的技巧被反复使用。例如，对于递归算法，您可以使用循环不变量。
另一个常见的技巧是将原始问题简化为算法的正确性证明更容易显示的问题，然后概括更简单的问题或表明更简单的问题可以转化为原始问题的解决方案。 这里是一个描述。
如果您心中有一个特定的算法，您可能会更好地询问如何构造该算法的证明而不是一般答案。
Usually proofs of correctness are very specific to the algorithm at hand.
However, there are several well known tricks that are used and re-used again. For example, with recursive algorithms you can use loop invariants.
Another common trick is reducing the original problem to a problem for which your algorithm's proof of correctness is easier to show, then either generalizing the easier problem or showing that the easier problem can be translated to a solution to the original problem. Here is a description.
If you have a particular algorithm in mind, you may do better in asking how to construct a proof for that algorithm rather than a general answer.
购买这些书籍： http://www.amazon.com/Science-Programming-Monographs- Computer/dp/0387964800
格里斯的书《科学规划》是很棒的东西。耐心、彻底、完整。
Buy these books: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
The Gries book, Scientific Programming is great stuff. Patient, thorough, complete.
Huth 和 Ryan 所著的《计算机科学中的逻辑》对用于验证系统的现代系统进行了合理可读的概述。曾几何时，人们讨论过用可能有也可能没有副作用的编程语言来证明程序的正确性。我从这本书和其他地方得到的印象是，实际应用程序是不同的——例如证明协议是正确的，或者芯片的浮点单元可以正确划分，或者用于操作链表的无锁例程是正确的。
ACM 计算调查第 41 卷第 4 期（2009 年 10 月）是关于软件验证的特刊。看起来，即使没有 ACM 帐户，您也可以通过搜索“形式化方法：实践和经验”来获取至少一篇论文。
Logic in Computer Science, by Huth and Ryan, gives a reasonably readable overview of modern systems for verifying systems. Once upon a time people talked about proving programs correct - with programming languages which may or may not have side effects. The impression I get from this book and elsewhere is that real applications are different - for instance proving that a protocol is correct, or that a chip's floating point unit can divide correctly, or that a lock-free routine for manipulating linked lists is correct.
ACM Computing Surveys Vol 41 Issue 4 (October 2009) is a special issue on software verification. It looks like you can get to at least one of the papers without an ACM account by searching for "Formal Methods: Practice and Experience".
Elazar 在评论中建议了工具 Frama-C 的演示视频，它为您提供了规范语言，ACSL，用于编写函数契约和各种分析器来验证C 函数满足其契约和安全属性，例如不存在运行时错误。
扩展教程ACSL 示例显示了实际 C 算法的示例被指定和验证，并将无副作用函数与有效函数分开（无副作用函数被认为更容易并且在教程中排在第一位）。该文档的另一个有趣之处在于它不是由其所描述的工具的设计者编写的，因此它对这些技术提供了更新鲜、更具有指导意义的视角。
The tool Frama-C, for which Elazar suggests a demo video in the comments, gives you a specification language, ACSL, for writing function contracts and various analyzers for verifying that a C function satisfies its contract and safety properties such as the absence of run-time errors.
An extended tutorial, ACSL by example, shows examples of actual C algorithms being specified and verified, and separates the side-effect-free functions from the effectful ones (the side-effect-free ones are considered easier and come first in the tutorial). This document is also interesting in that it was not written by the designers of the tools it describe, so it gives a fresher and more didactic look at these techniques.
如果您熟悉 LISP，那么您一定应该查看 ACL2： http ://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
If you are familiar with LISP then you should definitely check out ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
Dijkstra 的编程学科和他的 EWD 为形式验证作为编程科学奠定了基础。一个更简单的工作是 Wirth 的系统编程，它从使用验证的简单方法开始。 Wirth 使用 ISO 之前的 Pascal 语言； Dijkstra 使用类似于 Algol-68 的形式主义，称为 Guarded (GCL)。自 Dijkstra 和 Hoare 以来，形式验证已经成熟，但这些较旧的文本可能仍然是一个很好的起点。
Dijkstra's Discipline of Programming and his EWDs lay the foundation for formal verification as a science in programming. A simpler work is Wirth's Systematic Programming, which begins with the simple approach to using verification. Wirth uses pre-ISO Pascal for the language; Dijkstra uses an Algol-68-like formalism called Guarded (GCL). Formal verification has matured since Dijkstra and Hoare, but these older texts may still be a good starting point.
PVS工具是斯坦福大学的人开发的一个规范和验证系统。我研究了它，发现它对于定理证明非常有用。
PVS tool developed by Stanford guys is a specification and verification system. I worked on it and found it very useful for Theoram Proving.
WRT (1)，您可能必须以某种方式创建算法模型，以在程序变量中“捕获”算法的副作用，旨在对此类基于状态的副作用进行建模。
WRT (1), you will probably have to create a model of the algorithm in a way that "captures" the side-effects of the algorithm in a program variable intended to model such state-based side-effects.