首先，这是否仅适用于没有副作用的算法？
其次，我在哪里可以了解这个过程，有什么好书、文章等？
问问题
4925 次
11 回答
6
- 当不涉及副作用时，通常更容易验证/证明正确性，但这不是绝对要求。
- 您可能想查看一些文档以了解诸如Z之类的正式规范语言。正式规范本身并不是证明，但通常是证明的基础。
于 2010-01-27T19:13:04.647 回答
4
我认为验证算法的正确性将验证其是否符合规范。有一个理论计算机科学的分支称为形式方法，如果您需要尽可能接近证明，它可能就是您正在寻找的东西。来自维基百科，
形式化方法是一种特殊的基于数学的技术，用于软件和硬件系统的规范、开发和验证
您将能够从链接的 Wikipedia 页面上的大量链接和Formal Methods wiki中找到许多学习资源和工具。
于 2010-01-27T19:07:46.373 回答
2
购买这些书：http ://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
Gries 的书，科学编程是很棒的东西。耐心，彻底，完整。
于 2010-01-27T19:09:09.100 回答
1
Huth 和 Ryan 合着的 Logic in Computer Science 对用于验证系统的现代系统进行了合理易读的概述。曾几何时，人们谈论证明程序是正确的——使用可能有也可能没有副作用的编程语言。我从这本书和其他地方得到的印象是实际应用程序是不同的——例如证明协议是正确的，或者芯片的浮点单元可以正确划分，或者用于操作链表的无锁例程是正确的。
ACM Computing Surveys Vol 41 第 4 期（2009 年 10 月）是关于软件验证的特刊。通过搜索“正式方法：实践和经验”，您似乎可以在没有 ACM 帐户的情况下获得至少一篇论文。
于 2010-01-27T20:16:23.090 回答
1
工具Frama-C，Elazar 在评论中建议了一个演示视频，它为您提供了一种规范语言ACSL，用于编写函数合同和各种分析器，用于验证 C 函数是否满足其合同和安全属性，例如没有运行-时间错误。
扩展教程，ACSL by example，显示了指定和验证的实际 C 算法的示例，并将无副作用的函数与有效的函数分开（无副作用的函数被认为更容易并且在教程中首先出现） . 该文档也很有趣，因为它不是由它所描述的工具的设计者编写的，因此它对这些技术提供了一个更新鲜和更具指导性的看法。
于 2010-01-28T20:36:32.320 回答
1
如果您熟悉 LISP，那么您绝对应该查看 ACL2：http ://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
于 2010-02-04T01:30:28.180 回答
1
Dijkstra 的编程学科和他的 EWD 为形式验证作为编程科学奠定了基础。一个更简单的工作是 Wirth 的系统编程，它从使用验证的简单方法开始。Wirth 使用 pre-ISO Pascal 作为语言；Dijkstra 使用了一种类似于 Algol-68 的形式，称为 Guarded (GCL)。自 Dijkstra 和 Hoare 以来，形式验证已经成熟，但这些旧文本可能仍然是一个很好的起点。
于 2013-08-14T17:37:21.830 回答
0
斯坦福大学开发的 PVS 工具是一个规范和验证系统。我研究了它，发现它对 Theoram Proving 非常有用。
于 2013-10-16T20:28:32.533 回答
0
WRT (1)，您可能必须以某种方式创建算法模型，以便在程序变量中“捕获”算法的副作用，以便对这种基于状态的副作用进行建模。
于 2014-07-21T04:22:33.360 回答