Haskell 函数可以通过正确性属性进行证明/模型检查/验证吗？

Question

继续以下想法：是否有任何可证明的现实世界语言？< /a>

我不了解你，但我厌倦了编写我无法保证的代码。

在提出上述问题并得到惊人的答复（谢谢大家！）后，我有决定缩小我的搜索范围，寻找一种可证明的、实用的 Haskell 方法。我选择 Haskell 因为它实际上很有用（有 很多 web 框架 为其编写的，这似乎是一个很好的基准）并且我认为它足够严格，功能上，它可能是可证明的，或者至少允许测试不变量。

这就是我想要的（并且一直无法找到）

我想要一个框架，可以查看 Haskell 函数，添加，用伪代码编写：

add(a, b):
    return a + b

- 并检查某些不变量是否适用于每个执行状态。我更喜欢一些正式的证明，但我会满足于模型检查器之类的东西。
在此示例中，不变式是给定值 a 和 b，返回值始终为总和 a+b。

这是一个简单的例子，但我不认为这样的框架不可能存在。可以测试的函数的复杂性肯定会有一个上限（函数的 10 个字符串输入肯定需要很长时间！）但这将鼓励更仔细的函数设计，并且与使用其他形式没有什么不同方法。想象一下使用 Z 或 B，当您定义变量/集合时，您一定要确保为变量提供尽可能小的范围。如果您的 INT 永远不会超过 100，请确保对其进行初始化！我认为，像这样的技术以及适当的问题分解应该能够对像 Haskell 这样的纯函数语言进行令人满意的检查。

我对正式方法或 Haskell 还不是很有经验。让我知道我的想法是否合理，或者您认为 haskell 不适合？如果您建议使用其他语言，请确保它通过“has-a-web-framework”测试，并阅读原文 问题 :-)

Answer 1

好吧，既然你选择了 Haskell 路线，那么有几件事要开始：

• 你熟悉 库里-霍华德对应？基于此用于机器检查证明的系统在很多方面都是简单的函数式编程语言，具有非常强大的类型系统。

• 您熟悉为分析 Haskell 代码提供有用概念的抽象数学领域吗？各种各样的代数和一些范畴论出现了很多。

• 请记住，Haskell 与所有图灵完备语言一样，始终具有不终止的可能性。一般来说，证明某事永远比证明某事为真或取决于非终止值要困难得多。

如果您认真地寻求证明，而不仅仅是测试，那么这些都是需要记住的事情。基本规则是这样的：使无效状态导致编译器错误。首先防止无效数据被编码，然后让类型检查器为您完成繁琐的部分。

如果你想更进一步，如果我没记错的话，证明助手 Coq 有一个“摘录到Haskell”功能可让您证明关键函数的任意属性，然后将证明转换为 Haskell 代码。

对于直接在 Haskell 中完成花哨的类型系统工作，Oleg Kiselyov 是大师。您可以在他的网站上找到一些巧妙技巧的示例，例如更高级别的多态类型来编码静态证明数组边界检查。

对于更轻量级的东西，您可以执行诸如 使用类型级别证书之类的操作 将一条数据标记为已检查正确性。您仍然需要自己进行正确性检查，但其他代码至少可以依赖于知道某些数据实际上已被检查。

您可以采取的另一个步骤是，基于轻量级验证和奇特的类型系统技巧，利用 Haskell 作为嵌入的宿主语言这一事实​​ 域特定语言；首先构建一种经过严格限制的子语言（理想情况下，一种非图灵完备的子语言），您可以更轻松地证明其有用的属性，然后使用该 DSL 中的程序在整个程序中提供核心功能的关键部分。例如，您可以证明双参数函数是关联的，以便证明使用该函数并行减少项目集合的合理性（因为函数应用程序的顺序并不重要，只有参数的顺序）。

---

哦，最后一件事。关于避免 Haskell 确实包含的陷阱的一些建议，这些陷阱可能会破坏原本安全的代码：这里你的死敌是一般递归，IO monad和部分函数：

• 最后一个相对容易避免：不要编写它们，也不要使用它们。确保每组模式匹配都能处理所有可能的情况，并且切勿使用 error 或 undefined。唯一棘手的部分是避免可能导致错误的标准库函数。有些显然是不安全的，比如 fromJust :: Maybe a ->; a 或 head :: [a] -> a 但其他的可能更微妙。如果您发现自己编写的函数确实无法对某些输入值执行任何操作，那么您就允许输入类型对无效状态进行编码，并且需要首先修复该问题。

• 从表面上看，第二种情况很容易避免，方法是将内容分散到各种纯函数中，然后从 IO 表达式中使用这些函数。更好的方法是尽可能将整个程序移至纯代码中，以便可以使用除实际 I/O 之外的所有内容独立对其进行评估。仅当您需要由外部输入驱动的递归时，这才变得很棘手，这使我想到了最后一项：

• 明智之举：有根据的递归和富有成效的核心递归强>。始终确保递归函数要么从某个起点到已知的基本情况，要么根据需要生成一系列元素。在纯代码中，最简单的方法是递归地折叠有限的数据结构（例如，不是在将计数器递增到某个最大值时直接调用自身的函数，而是创建一个包含计数器值范围的列表并将其折叠）或递归生成惰性数据结构（例如，某个值的渐进近似列表），同时小心地不要直接混合两者（例如，不要只是“查找流中满足某些条件的第一个元素”；它可能不会相反，从流中获取值到某个最大深度，然后搜索有限列表，适当处理未找到的情况）。

• 结合最后两项，对于真正需要 IO 和一般递归的部分，尝试将程序构建为增量组件，然后将所有尴尬的部分压缩为单个“驱动程序”功能。例如，您可以使用诸如 mainLoop :: UIState -> 之类的纯函数编写 GUI 事件循环。活动-> UIState，退出测试，如 quitMessage :: Events -> Bool，获取挂起事件的函数getEvents::IO Events，以及更新函数updateUI::UIState -> IO ()，然后使用像 runLoopIO :: (b -> a -> b) ->; 这样的通用函数实际运行该东西。 b-> IO一-> (b→IO())→ IO()。这使复杂的部分真正保持纯粹，让您可以使用事件脚本运行整个程序并检查生成的 UI 状态，同时将笨拙的递归 I/O 部分隔离为单个抽象函数，该函数易于理解并且通常不可避免地是正确的结合

Answer 2

可能最接近您要求的是 Haskabelle，证明助手 Isabelle 附带的工具，可以翻译 Haskell 文件进入伊莎贝尔理论并让你证明有关它们的东西。据我了解，这个工具是在 HOL - ML - Haskell 项目和 中开发的文档页面包含一些有关背后理论的信息。

我对这个项目不是很熟悉，也不太了解它做了什么。但我知道 Brian Huffman 一直在玩这些东西，查看他的论文并会谈，它们应该包含相关内容。

Answer 3

我不确定你所要求的是否真的能让你快乐。 :-)

对通用语言进行模型检查几乎是不可能的，因为模型必须是特定领域才能实用。由于哥德尔不完备定理，没有方法可以在足够表达的逻辑中自动找到证明。

这意味着您必须自己编写证明，这就提出了这样的问题：这些努力是否值得花费时间。当然，这种努力创造了非常有价值的东西，即保证您的程序是正确的。问题不在于这是否是必须具备的，而在于花费的时间成本是否太大。关于证明的问题是，虽然您可能“直观”地理解您的程序是正确的，但通常很难将这种理解形式化作为证明。直觉理解的问题在于它很容易出现意外错误（打字错误和其他愚蠢的错误）。这是编写正确程序的基本困境。

因此，关于程序正确性的研究就是让证明更容易形式化并自动检查其正确性。编程是“易于形式化”的一个组成部分；以易于推理的方式编写程序非常重要。目前，我们有以下范围：

• 命令式语言，如 C、C++、Fortran、Python：在这里很难将任何内容形式化。单元测试和一般推理是获得至少一些保证的唯一方法。静态类型仅捕获微不足道的错误（这比不捕获它们要好得多！）。

• 像 Haskell、ML 这样的纯函数式语言：富有表现力的类型系统有助于捕获重要的 bug 和错误。我想说，对于最多 200 行左右的片段，手动证明正确性是很实用的。 （例如，我为我的操作包做了证明。）Quickcheck 测试是形式化证明的廉价替代品。

• 依赖类型语言和证明助手，如 Agda、Epigram、Coq：借助证明形式化和发现的自动化帮助，证明整个程序的正确性成为可能。然而，负担仍然很高。

在我看来，当前编写正确程序的最佳点是纯函数式编程。如果生命取决于程序的正确性，那么你最好升级到更高的级别并使用证明助手。

Answer 4

听起来你想要 ESC/Haskell： http:// /research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm

哦，Agda 现在确实有一个 Web 框架（至少是概念证明）：http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/< /a>

Answer 5

你看似简单的例子，add(a,b)，实际上很难验证——浮点、溢出、下溢、中断、编译器是否验证、硬件是否验证等等

。 galois.com/blog/2010/05/12/tech-talk-development-good-habits-for-bare-metal-programming/" rel="nofollow">Habit 是 Haskell 的一种简化方言，它允许用于证明程序属性。

休谟是一种有 5 个级别的语言，每个级别都更有限因此更容易验证：

Full Hume
  Full recursion
PR−Hume
  Primitive Recursive functions
Template−Hume
  Predefined higher−order functions
  Inductive data structures
  Inductive  Non−recursive first−order functions
FSM−Hume
  Non−recursive data structures
HW−Hume
  No functions
  Non−recursive data structures

当然，当今证明程序属性最流行的方法是单元测试，它提供了强有力的定理，但这些定理过于具体。 “被认为有害的类型”，皮尔斯，幻灯片 66

Answer 6

看看 Zeno。引用维基页面：

Zeno 是 Haskell 程序属性的自动证明系统；由 William Sonnex、Sophia Drossopoulou 和 Susan Eisenbach 在伦敦帝国理工学院开发。它旨在解决任何输入值的两个 Haskell 项之间相等的一般问题。

当今可用的许多程序验证工具都属于模型检查类型；能够非常快速地遍历非常大但有限的搜索空间。这些非常适合解决具有大量描述但没有递归数据类型的问题。另一方面，Zeno 旨在归纳证明无限搜索空间上的属性，但仅限于那些具有小且简单规范的属性。

Answer 7

当然可以正式证明 Haskell 程序的一些属性。我在 FP 考试中必须这样做：给定两个表达式，证明它们表示相同的函数。一般来说这是不可能的，因为 Haskell 是图灵完备的，所以任何机械证明器要么必须是证明助手（带有用户指导的半自动），要么是模型检查器。

在这个方向上已经进行了尝试，请参见 P-logic: property Haskell 程序验证 或使用 Mizar 证明函数式程序的正确性。这两篇学术论文更多的是描述方法而不是实现。

Answer 8

剑桥MSR最近的一些努力：
http://research.microsoft.com /en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

Answer 9

工具AProVE（至少）能够证明Haskell程序的终止，这是证明的一部分正确性。
更多信息请参阅本文 (较短版本）。

除此之外，您可能对依赖类型感兴趣。在这里，类型系统被扩展并用于使错误的程序成为不可能。

Answer 10

您可以使用工具hs-to-coq将 Haskell 大部分自动转换为 Coq，然后使用 Coq 证明助手的全部功能来验证您的 Haskell 代码。请参阅论文 https://arxiv.org/abs/1803.06960 和 https://arxiv.org/abs/1711.09286 了解更多信息。