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

Question

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

在问了上述问题并得到了惊人的回应（谢谢大家！）之后，我决定缩小对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”测试，并阅读原始问题:-)

score 63 · Accepted Answer

好吧，因为您采用的是 Haskell 路线，所以要从几件事开始：

你熟悉库里-霍华德的对应关系吗？有一些用于基于此的机器检查证明的系统，在许多方面，它们只是具有非常强大的类型系统的函数式编程语言。
您是否熟悉为分析 Haskell 代码提供有用概念的抽象数学领域？各种各样的代数和一些范畴论出现了很多。
请记住，Haskell 和所有图灵完备的语言一样，总是有不终止的可能性。一般来说，证明某事永远为真比证明某事为真或取决于非终止值要困难得多。

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

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

对于直接在 Haskell 中做花哨的类型系统的东西，Oleg Kiselyov 是大师。你可以在他的网站上找到一些巧妙技巧的例子，比如更高等级的多态类型来编码数组边界检查的静态证明。

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

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

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

最后一个相对容易避免：不要编写它们，也不要使用它们。确保每组模式匹配处理所有可能的情况，并且永远不要使用erroror undefined。唯一棘手的部分是避免可能导致错误的标准库函数。有些显然是不安全的，例如fromJust :: Maybe a -> a或head :: [a] -> a但有些可能更微妙。如果您发现自己编写的函数确实无法对某些输入值执行任何操作，那么您将允许输入类型对无效状态进行编码，并且需要首先修复它。
第二种方法很容易在表面上避免，方法是通过各种纯函数分散内容，然后从IO表达式中使用这些纯函数。更好的是，尽可能将整个程序移到纯代码中，以便可以使用除实际 I/O 之外的所有内容独立评估它。仅当您需要由外部输入驱动的递归时，这才变得很棘手，这使我想到了最后一项：
智者的话：有根据的递归和富有成效的核心递归. 始终确保递归函数要么从某个起点转到已知的基本案例，要么按需生成一系列元素。在纯代码中，最简单的方法是递归地折叠有限的数据结构（例如，在将计数器递增到某个最大值时，不是直接调用自身的函数，而是创建一个包含计数器值范围的列表并将其折叠起来）或递归生成惰性数据结构（例如，某个值的渐进近似列表），同时小心地不要直接将两者混合（例如，不要只是“找到满足某些条件的流中的第一个元素”；它可能不会相反，从流中取值直到某个最大深度，然后搜索有限列表，适当地处理未找到的情况）。
结合最后两项，对于您真正需要IO使用一般递归的部分，尝试将程序构建为增量组件，然后将所有笨拙的部分压缩为单个“驱动程序”函数。例如，您可以使用纯函数（如mainLoop :: UIState -> Events -> UIState）、退出测试（如quitMessage :: Events -> Bool）、获取挂起事件getEvents :: IO Events的函数和更新函数（update）编写 GUI 事件循环updateUI :: UIState -> IO ()，然后使用通用函数（如runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO (). 这使复杂的部分真正保持纯净，让您使用事件脚本运行整个程序并检查生成的 UI 状态，同时将笨拙的递归 I/O 部分隔离为一个易于理解且通常不可避免地正确的单一抽象函数通过参数化。

score 21 · Accepted Answer

可能与您所要求的最接近的是Haskabelle，这是一个与证明助手Isabelle一起提供的工具，它可以将 Haskell 文件转换为 Isabelle 理论，并让您证明有关它们的东西。据我了解，该工具是在 HOL - ML - Haskell 项目中开发的，文档页面包含有关背后理论的一些信息。

我对这个项目不是很熟悉，对它做了什么也不太了解。但我知道布赖恩霍夫曼一直在玩这些东西，看看他的论文和演讲，它们应该包含相关的东西。

score 19 · Accepted Answer

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

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

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

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

命令式语言，如 C、C++、Fortran、Python：在这里很难将任何东西形式化。单元测试和一般推理是获得至少一些保证的唯一方法。静态类型只捕获微不足道的错误（这比不捕获它们要好得多！）。
像 Haskell、ML 这样的纯函数式语言：表达性类型系统有助于捕捉重要的错误和错误。我会说，手动证明正确性对于大约 200 行的片段是实用的。（例如，我为我的操作包做了证明。）Quickcheck测试是形式化证明的廉价替代品。
依赖类型语言和 Agda、Epigram、Coq 等证明助手：借助证明形式化和发现的自动化帮助，证明整个程序的正确性成为可能。但是，负担仍然很大。

在我看来，目前编写正确程序的最佳点是纯粹的函数式编程。如果生命取决于程序的正确性，那么您最好再上一层楼并使用证明助手。

score 5 · Accepted Answer

听起来你想要 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/

score 4 · Accepted Answer

你看过快速检查吗？它可能会提供您需要的一些东西。

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

score 3 · Accepted Answer

您看似简单的示例 add(a,b) 实际上很难验证 - 浮点、上溢、下溢、中断、编译器是否已验证、硬件是否已验证等。

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

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

完全休谟
  完全递归
PR-休谟
  原始递归函数
模板-休谟
  预定义的高阶函数
  归纳数据结构
  归纳非递归一阶函数
FSM-休谟
  非递归数据结构
HW-休谟
  无功能
  非递归数据结构

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

score 3 · Accepted Answer

看看芝诺。引用维基页面：

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

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

score 2 · Accepted Answer

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

在这个方向上已经进行了尝试，请参见例如P-logic：Haskell 程序的属性验证或使用 Mizar 证明功能程序的正确性。两者都是描述方法多于实现的学术论文。

score 1 · Accepted Answer

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

score 1 · Accepted Answer

AProVE工具（至少）能够证明 Haskell 程序的终止，这是证明正确性的一部分。可以在本文中找到更多信息（较短的版本）。

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

score 1 · Accepted Answer

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

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

11 回答 11

Related

Reference