我在大学里学习过形式系统，但令我失望的是，它们似乎并没有真正用于现实世界。
我喜欢能够知道某些代码（对象、函数等）工作的想法，而不是通过测试，而是通过证明。
我相信我们都熟悉物理工程和软件工程之间不存在的相似之处（钢的行为可以预测，软件可以做任何事情——谁知道呢！），我很想知道是否有任何语言可以可以在实际中使用（要求 Web 框架要求太多了吗？）
我听说过有关 scala 等函数式语言的可测试性的有趣事情。
作为软件工程师，我们有哪些选择？
问问题
9066 次
11 回答
39
是的，有些语言是为编写可证明正确的软件而设计的。有些甚至用于工业。Spark Ada可能是最突出的例子。我与 Praxis Critical Systems Limited 的一些人交谈过，他们将它用于在 Boings 上运行的代码（用于引擎监控），它看起来相当不错。（这里是对语言的一个很好的总结/描述。）这种语言和随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！
我的印象和经验是编写正确的软件有两种技巧：
技巧 1：用您熟悉的语言（例如 C、C++ 或 Java）编写软件。采用这种语言的正式规范，并证明您的程序是正确的。
如果您的目标是 100% 正确（这通常是汽车/航空航天行业的要求），那么您将花费很少的时间进行编程，而花更多的时间来证明。
技巧 2：用稍微笨拙的语言（例如 Ada 的某个子集或 OCaml 的调整版本）编写软件，并在此过程中编写正确性证明。在这里，编程和证明齐头并进。Coq 中的编程甚至完全等同于它们！（见库里-霍华德对应）
在这些情况下，您总是会得到一个正确的程序。（错误将保证植根于规范中。）您可能会花更多时间在编程上，但另一方面，您会在此过程中证明它是正确的。
请注意，这两种方法都取决于您手头有正式规范（否则您将如何判断什么是正确/不正确行为）和正式定义的语言语义（否则您将如何判断实际行为你的程序是）。
这里还有一些正式方法的例子。如果它是“真实世界”，取决于你问谁:-)
- Coq 定理证明器：使用 Coq 编程（技术 2）
- ESC/Java（技术 1，虽然不完善也不完整）
- Spec#（技术 1，虽然不完善也不完整）
- 为什么 / Krakatoa（技术 2，基于 Java）
我只知道一种“可证明正确”的网络应用程序语言：UR。“通过编译器”的 Ur 程序保证不会：
- 遭受任何类型的代码注入攻击
- 返回无效的 HTML
- 包含无效的应用程序内链接
- HTML 表单与其处理程序预期的字段不匹配
- 包括对远程 Web 服务器提供的“AJAX”样式服务做出错误假设的客户端代码
- 尝试无效的 SQL 查询
- 在与 SQL 数据库或浏览器和 Web 服务器之间的通信中使用不正确的编组或解组
于 2010-10-31T21:13:41.020 回答
24
为了回答这个问题，您确实需要定义“可证明”的含义。正如 Ricky 所指出的，任何具有类型系统的语言都是一种具有内置证明系统的语言，该证明系统在您每次编译程序时都会运行。可悲的是，这些证明系统几乎总是无能为力——回答诸如Stringvs之类的问题Int并避免诸如“列表排序了吗？”之类的问题。——但它们仍然是证明系统。
不幸的是，您的证明目标越复杂，使用可以检查您的证明的系统就越难。当您考虑到在图灵机上不可判定的问题类别的绝对规模时，这很快就会升级为不可判定性。当然，理论上你可以做一些基本的事情，比如证明你的排序算法的正确性，但除此之外的任何事情都将是如履薄冰。
即使是为了证明排序算法的正确性这样简单的事情，也需要一个相对复杂的证明系统。（注意：由于我们已经确定类型系统是语言中内置的证明系统，所以我将用类型理论来谈论事情，而不是更加有力地挥手）我相当肯定列表排序的完全正确性证明需要某种形式的依赖类型，否则您无法在类型级别引用相对值。这立即开始进入类型理论的领域，这些领域已被证明是不可判定的。因此，虽然您可以证明列表排序算法的正确性，但唯一的方法是使用一个系统，该系统还允许您表达无法验证的证明。亲自，
还有我之前提到的易用性方面。您的类型系统越复杂，使用起来就越不愉快。这不是一个硬性规定，但我认为它在大多数情况下都是正确的。与任何正式系统一样，您经常会发现表达证明比一开始就创建实现需要更多的工作（并且更容易出错）。
除了所有这些，值得注意的是 Scala 的类型系统（如 Haskell 的）是图灵完备的，这意味着理论上您可以使用它来证明您的代码的任何可判定属性，前提是您已经以这样的方式编写了代码方式，它是服从这样的证明。Haskell 几乎可以肯定是比 Java 更好的语言（因为 Haskell 中的类型级编程类似于 Prolog，而 Scala 中的类型级编程更类似于 SML）。我不建议您以这种方式使用 Scala 或 Haskell 的类型系统（算法正确性的正式证明），但该选项在理论上是可用的。
总而言之，我认为你没有在“现实世界”中看到形式系统的原因在于形式证明系统已经屈服于实用主义的无情暴政。正如我所提到的，制作正确性证明需要付出如此多的努力，以至于几乎不值得。业界很久以前就决定创建临时测试比通过任何类型的分析形式推理过程更容易。
于 2010-10-31T22:42:05.690 回答
10
你问了一个我们很多人多年来都问过的问题。我不知道我有一个好的答案，但这里有一些：
有一些易于理解的语言有可能在今天得到证明；通过 ACL2 的 Lisp 就是其中之一，当然 Scheme 也有一个很好理解的正式定义。
许多系统都尝试使用纯函数式语言，或者几乎是纯函数式语言，例如 Haskell。Haskell 中有相当多的形式化方法可用。
追溯到 20 多年前，使用手证明形式语言的时间很短，然后将其严格翻译成编译语言。一些例子是 IBM 的 Software Cleanroom、ACL、Gypsy 和 Rose out of Computational Logic，John McHugh 和我在可信赖的 C 编译方面的工作，以及我自己在 C 系统编程的手工证明方面的工作。这些都得到了一些关注，但没有一个人将其付诸实践。
我认为，一个有趣的问题是，将正式方法付诸实践的充分条件是什么？我很想听听一些建议。
于 2010-10-31T21:09:19.917 回答
9
打字语言证明不存在某些类别的错误。类型系统越先进，它们可以证明不存在的错误就越多。
为了证明整个程序有效，是的，您正在超越数学和编程相互交汇的普通语言的界限，握手，然后继续使用希腊符号谈论程序员如何无法处理希腊符号。无论如何，这就是它的Σ。
于 2010-10-31T21:00:08.530 回答
4
这种可证明的语言在现实世界中的使用将非常难以编写和理解。商业世界需要快速运行的软件。
“可证明的”语言只是不能用于编写/读取大型项目的代码库，而且似乎只适用于小型和孤立的用例。
于 2010-10-31T22:50:44.843 回答
4
我参与了两种可证明的语言。第一个是 Perfect Developer 支持的语言，这是一个指定软件、改进软件和生成代码的系统。它已被用于一些大型系统，包括 PD 本身，并且在许多大学中教授。我参与的第二种可证明语言是 MISRA-C 的可证明子集，请参阅C/C++ 验证博客了解更多信息。
于 2011-02-10T01:50:57.253 回答
3
您可以研究像 Haskell 这样的纯函数式语言，当您的要求之一是可证明性时使用这些语言。
如果您对函数式编程语言和纯函数式编程语言感兴趣，这是一本有趣的书。
于 2010-10-31T21:08:32.190 回答
3
Scala 旨在成为“现实世界”，因此没有努力使其可证明。你可以在 Scala 中做的是生成函数式代码。功能代码更容易测试，恕我直言，这是“现实世界”和可证明性之间的一个很好的折衷方案。
编辑 ===== 删除了我关于 ML 是“可证明的”的错误想法。
于 2010-10-31T22:09:24.210 回答
3
在可证明正确的代码的上下文中，我对“真实世界”的（有争议的）定义是：
- 它必须涉及某种程度的自动化，否则你将花费太多时间来证明和处理混乱的小细节，而且这将是完全不切实际的（可能除了航天器控制软件之类的东西，你可能实际上想在细致的支票上花费百万美元）。
- 它必须支持某种程度的函数式编程，这有助于您编写非常模块化、可重用且易于推理的代码。显然，编写或证明 Hello World 或各种简单程序不需要函数式编程，但在某一点上，函数式编程确实变得非常有用。
- 虽然您不一定必须能够用主流编程语言编写代码，但作为替代方案，您至少应该能够将您的代码机器翻译成以主流编程语言编写的相当有效的代码，并且可靠方式。
以上是比较普遍的要求。其他的，例如对命令式代码建模的能力，或者证明高阶函数正确的能力，对于某些任务可能很重要或必不可少，但不是全部。
鉴于这些观点，我的这篇博文中列出的许多工具可能很有用——尽管它们几乎都是新的和实验性的，或者对于绝大多数行业程序员来说并不熟悉。不过，那里涵盖了一些非常成熟的工具。
于 2012-06-10T12:13:41.440 回答
2
作为一个很好的现实生活示例，有一个项目旨在提供一个用 Agda 编写的经过验证的 HTTP REST 库，名为 Lemmachine：https ://github.com/larrytheliquid/Lemmachine
于 2015-01-27T00:57:51.460 回答