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

Question

继续探讨： 有没有可以证明实际可用的语言？

我不知道你怎么看，但是我已经厌倦了编写无法保证质量的代码。

在提出以上问题并得到惊人回应后（感谢大家！），我决定将我的搜索范围缩小到一种可证明、实用、实用的方法，即Haskell。我选择 Haskell 是因为它实际上很有用（有许多Web框架用它编写，并且这似乎是一个很好的基准）而且我认为它在函数上足够严格，功能性很高，可能是可证明的，或者至少允许不变式测试。

以下是我想要的内容 （但一直没找到）：

我想要一个框架，能够查看一个 Haskell 函数，添加如下伪代码：

add(a, b):
    return a + b

- 并检查每个执行状态是否保持某些不变量。我希望有一些正式的证明，但如果有像模型检查器这样的东西，我也可以接受。
在这个例子中，不变量将是给定值a和b时，返回值总是和a+b相等。

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

我还不太熟悉形式化方法或Haskell。如果您认为我的想法是可行的，或者您认为Haskell不适合，那请告诉我。如果您建议使用其他语言，请确保它通过了“具有Web框架”测试，并阅读原始的问题 :-)

- 0atman

---

@Steven: 真的吗？为什么会这样？如果一段代码已被证明具有某种属性，那么无论它与哪些其他代码进行交互，它始终具有该属性，您可以在其他证明中依赖于该属性。证明是可重复使用和组合的，而测试则不是，通过将证明编码在类型系统中，就不可能让它们与代码本身不同步。 - C. A. McCann

@Steven：是的，我同意camccann的观点，我不需要测试房子中每个砖块的组合。不过那只山羊真漂亮！ - 0atman

@Steven：他们并不需要，这就是整个关键！如果一个函数对所有可能的输入都可以被证明是正确的，那么使用它所需的唯一义务就是提供适当类型的参数。不必担心集成点的问题，这正是类型编码证明具有组合性的原因。知道一段代码保证永远不会失败或产生运行时错误，这就是静态类型的好处。 - C. A. McCann

@Steven：就我个人而言，我宁愿花更长时间编写不会出错的代码，而不是编写不可靠的代码，然后浪费时间编写琐碎的测试和担心可能出现的问题...但我想每个人都有自己的做法！ - C. A. McCann

谢谢大家的意见，可以把它们带到论坛上继续讨论。 - 0atman

Answer 1

首先，如果你选择使用Haskell编程语言：

• 你是否熟悉Curry-Howard correspondence？基于此的机器检查证明系统在很多方面上都是具备强大类型系统的函数式编程语言。

• 你是否熟悉提供有用概念分析Haskell代码的抽象数学领域？各种代数和范畴理论的一些部分常常被提及。

• 请记住，像所有图灵完备的语言一样，Haskell总是存在非终止的可能性。通常情况下，证明某些事情将始终成立比证明某些事情将成立或依赖于非终止值要困难得多。

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

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

如果你想在Haskell中进行高级类型系统编程，Oleg Kiselyov是大师级人物。你可以在他的网站上找到一些例子，比如 使用高阶多态类型来编码数组边界检查的静态证明。

对于更轻量级的东西，你可以使用 类型级证书 标记数据已经被检查过了。虽然正确性检查仍然由你自己完成，但其他代码至少可以依赖于知道某些数据已经被检查过了。

另一个步骤是，在轻量级验证和高级类型系统技巧的基础上，利用Haskell作为嵌入 特定领域语言 的主机语言的优势；首先构建一个严格限制的子语言（理想情况下，这个子语言不是图灵完备的），然后使用该DSL中的程序来提供整个程序的关键核心功能。例如，你可以证明一个二元函数是可结合的，以此来证明使用该函数并行化减少集合项时是正确的（因为函数应用的顺序不重要，只有参数的顺序重要）。

---

哦，最后一件事。关于避免Haskell中可能会破坏本来可以安全构建的代码的陷阱，给出一些建议：你的宿敌是普通递归、IO单子和部分函数：

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

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

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

• 结合最后两个项目，在那些确实需要带有通用递归的IO部分中，尝试将程序构建为增量组件，然后将所有棘手的部分压缩成一个单独的“驱动”函数。例如，您可以使用一个纯函数编写GUI事件循环，如mainLoop :: UIState -> Events -> UIState，一个退出测试如quitMessage :: Events -> Bool，一个获取挂起事件的函数getEvents :: IO Events，以及一个更新函数updateUI :: UIState -> IO ()，然后使用类似runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO ()的通用函数实际运行程序。这使得复杂部分真正纯净，让您可以使用事件脚本运行整个程序并检查结果的UI状态，同时将棘手的递归I/O部分隔离到单个抽象函数中，易于理解，并且通常会通过parametricity无法避免。

- C. A. McCann

---

谢谢，你认为直接对Haskell进行模型检查是可能的吗？ - 0atman

@Oatman：通常情况下，我们可以像对待任何编程语言一样进行模型检查。由于 Haskell 具有纯度和类型安全性，许多用于减少或简化要检查的状态空间的技术在 Haskell 中很容易或自动实现。然而，在这里考虑状态转换可能是适得其反的。 - C. A. McCann

@Oatman：实际上，Haskell 在这方面的主要优势在于不需要外部工具就能实现很多功能。只要尽可能避免使用IO、一般递归和部分函数（对于大多数程序而言，这几乎是“几乎所有地方，稍加努力即可”）。 - C. A. McCann

@camccann：我喜欢这个领域特定的想法。一个专门设计用于证明的Haskell方言！这是我必须尝试一下的东西吗？或者据你所知，类似的工作已经完成了吗？ - 0atman

@Oatman：天哪，Haskell程序员真是痴迷于程序的正确性。你可以在各个地方找到这种小片段；例如，IO单子的整个目的就是在惰性求值的情况下提供有序的副作用，同时不让纯代码观察到任何不纯洁的东西。但如果你想要更深入的例子，可以看看Hackage上的ImProve。 - C. A. McCann

Coq确实具有“提取到Haskell”的功能。 - Tom Crockett

Answer 2

您所需的最接近的工具可能是Haskabelle，它是随附于证明助手Isabelle的一项工具，可以将Haskell文件转换为Isabelle理论，并允许您对其进行证明。据我了解，这个工具是在HOL-ML-Haskell项目中开发的，文档页面包含一些关于其中的背后理论的信息。

我对这个项目不是特别熟悉，也不太清楚它做了什么。但是我知道Brian Huffman一直在尝试这些东西，请查看他的论文和演讲，应该包含相关内容。

- svenningsson

---

谢谢，我会去看看的，不过我真的在寻找一种纯语言的模型检查方法。将更正式的语言翻译成Haskell并不是通用使用的最佳选择。 - 0atman

不，恰恰相反。Haskell 被翻译成 Isabelle。这种方法可能仍不是最佳的，但对于您的目的来说，它可能比 Coq 生成 Haskell 更好。 - svenningsson

哦哦哦！抱歉我误读了你的回答。嗯，这很不寻常，但更有用！ - 0atman

Answer 3

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

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

这意味着你必须自己撰写证明，这就引出了一个问题：投入的努力是否值得花费。当然，这样做会创造出非常有价值的东西，即确保程序正确性的保证。问题不在于这是否必不可少，而在于耗费的时间是否太大。证明的问题在于，虽然你可能有"直观"的理解你的程序是正确的，但通常很难将这种理解形式化为证明。直观理解的问题在于它极易受到意外错误（打字和其他愚蠢的错误）的影响。这是编写正确程序的基本困境。

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

• 类似C、C++、Fortran、Python的命令式语言：在这里形式化任何东西都非常困难。单元测试和一般推理是获得至少某些确保的唯一方法。静态类型只能捕获微不足道的错误（比不捕获好多了！）。

• 类似Haskell、ML的纯函数语言：表达力很强的类型系统有助于发现非微不足道的错误和错误。手动证明正确性对于不超过大约200行的代码片段来说是实用的，我想。（例如，我为我的操作库做了一个证明。）快速检查是形式化证明的廉价替代品。

• 依赖类型语言和证明助手（如Agda、Epigram、Coq）：通过自动的证明形式化和发现，整个程序正确性的证明是可能的。然而，负担仍然很重。

在我看来，编写正确程序的当前最佳实践是 纯函数式编程。如果生命取决于您的程序的正确性，那么最好再提高一个层次并使用证明助手。

- Heinrich Apfelmus

---

作为一个可能有点苛刻的人，你可能是指“没有有效的方法”，因为可以通过逐步枚举和测试越来越长的证明来解决问题，可能会受到某种递增的“燃料”限制以避免停机陷阱 :-) - sclv

这里是解决停机问题的一种方法：无限运行程序，并等待看它是否最终停止。在列举证明时如何知道何时停止？简而言之，你可以用这种方式来“寻找”证明，但你无法区分“不存在证明”和“尚未找到证明”。 - C. A. McCann

我选择了一个适当的“方法”定义，其中已经包含了效率方面的考虑。;-) - Heinrich Apfelmus

此外，Haskell 的 SmallCheck 库可以对 Enum 上的一系列值进行穷举式检查。这对于一次性验证某些 Enum 属性的实用性非常高，不需要为每个构建重新计算。 - recursion.ninja

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/

- sclv

---

ESC/Haskell看起来不错，尽管实现是理论的和有些有限的，根据我浏览论文的经验。然而，这是一个很好的资源 - 谢谢！ - 0atman

GHC 什么时候会支持 ESC/Haskell？ - dan_waterworth

@dan_waterworth -- 不幸的是，我不知道任何在这方面的计划。 - sclv

很遗憾，我真的需要它来完成我正在进行的项目。感谢您的回复。 - dan_waterworth

Answer 5

你是否看过quickcheck？它可能提供你需要的一些东西。

http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck

- Jonno_FTW

---

是的，我认为它看起来很棒，绝对会成为我进一步研究的基础。 - 0atman

还有一个叫做smallcheck的工具- smallcheck类似于quickcheck，但它专注于对“小”案例进行穷尽测试，针对可配置的“小”的概念。 - mokus

我还记得在某个地方看到过一个包，它可以自动根据代数属性生成quickcheck测试。例如，声明两个函数的分配律将会产生检查，即f x (g y z)总是等于g (f x y) (f x z)。 - C. A. McCann

还可以看看Lazy Smallcheck，它利用了Haskell的惰性求值。 - Robin Green

Answer 6

你所提供的一个看似简单的例子，add(a,b)，实际上很难进行验证 - 浮点数，溢出，下溢，中断，编译器是否经过验证，硬件是否经过验证等等。

Habit是Haskell的一种简化方言，允许证明程序属性。

Hume是一种语言，具有5个级别，每个级别都更加有限，因此更容易验证：

完整的Hume
  完全递归
PR−Hume
  原始递归函数
Template−Hume
  预定义的高阶函数
  归纳数据结构
  归纳非递归一阶函数
FSM−Hume
  非递归数据结构
HW−Hume
  没有函数
  非递归数据结构

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

- ja.

---

算术可能会成为一个问题。从理论上讲，如果您知道所有结果的大小，包括中间结果，那么您可以做出保证。实际上，许多计算并不适合这种情况。如果没有任意大小的整数，证明算术正确性就很棘手。对于浮点数，请参考http://docs.sun.com/source/806-3568/ncg_goldberg.html（每个计算机科学家都应该了解的浮点数知识），而且这是在许多非常聪明的人试图使浮点数可行之后。 - David Thornley

Answer 7

请看 Zeno，引用维基页面：

Zeno是一种 Haskell 程序属性自动证明系统；由威廉·桑内克斯（William Sonnex）、索菲亚·德罗索普卢（Sophia Drossopoulou）和苏珊·艾森巴赫（Susan Eisenbach）在伦敦帝国理工学院开发。它旨在解决任何输入值下两个 Haskell 术语之间相等的一般问题。

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

- Petr

Answer 8

“有些”Haskell程序的属性是可以形式化证明的。我在我的FP考试中不得不这样做：给定两个表达式，证明它们表示相同的函数。通常情况下这是不可能的，因为Haskell是图灵完备的，所以任何机械证明者要么是一个证明助手（半自动与用户指导），要么是一个模型检测器。

在此方向上已经有一些尝试，例如参见P-logic: property verification for Haskell programs 或 Proving the correctness of functional programs using Mizar。两篇论文都描述了方法而不是实现。

- Fred Foo

---

我想补充一点，考试时我至少感觉像一个机械定理证明器 ;) - Fred Foo

哎呀，谷歌搜索“mizar haskell”的第二个结果是这个stackoverflow问题！1 :-( - 0atman

这只是通过Google和CiteseerX的快速搜索。这篇Mizar论文发表在学术期刊上，但并不是高知名度的期刊。 - Fred Foo

@Oatman：这不意味着太多。Stack Overflow非常受欢迎。涉及小众话题的问题往往能轻松超越一手资料。 - C. A. McCann

非常正确，但是关于Mizar的信息非常稀少，不是我所希望的预先存在的软件包。我会把它加入我的阅读列表！ - 0atman

Answer 9

一些由微软剑桥研究院最近做出的努力： http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

- rsinha

Answer 10

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

- Joachim Breitner