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

Question

继续从以下想法开始:Are there any provable real-world languages?

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

在提出上述问题并得到了惊人的回应(谢谢大家!)后，我决定缩小对 Haskell 的可证明的、务实的方法的搜索范围。 .我选择 Haskell 是因为它实际上很有用(有 many web frameworks 为它写的，这似乎是一个很好的基准)和 我觉得已经够严格了，functionally ，它可能是可证明的，或者至少允许测试不变量。

这就是我想要的 (并且一直找不到)

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

add(a, b):
    return a + b

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

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

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

Answer 1

好吧，有几件事要开始，因为你走的是 Haskell 路线:

您熟悉Curry-Howard correspondence吗？ ?有一些系统用于基于此的机器检查证明，这些系统在许多方面都是具有非常强大的类型系统的简单函数式编程语言。

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

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

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

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

直接在 Haskell 中做花哨的类型系统的东西， Oleg Kiselyov is the Grand Master .你可以在他的网站上找到像 higher-rank polymorphic types to encode static proofs of array bounds checking 这样的巧妙技巧的例子。 .

对于更轻量级的东西，你可以做这样的事情 using a type-level certificate将一段数据标记为已检查正确性。您仍然需要自己进行正确性检查，但其他代码至少可以依赖于知道某些数据实际上已经过检查。

在轻量级验证和花哨的类型系统技巧的基础上，您可以采取的另一个步骤是利用 Haskell 作为嵌入的宿主语言运行良好的事实 domain-specific languages ;首先构建一个仔细限制的子语言(理想情况下，一个不是图灵完备的)你可以更容易地证明有用的属性，然后使用该 DSL 中的程序来提供整个程序中的关键核心功能。例如，您可以证明一个双参数函数是关联的，以便证明使用该函数对项目集合进行并行归约是合理的(因为函数应用程序的顺序无关紧要，只有参数的顺序无关紧要)。

哦，最后一件事。关于避免 Haskell 确实包含的陷阱的一些建议，这些陷阱可能破坏本来可以安全构建的代码:您的死敌是 一般递归 , IO monad , 和 偏函数 :

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

第二个很容易在表面上避免，方法是通过各种纯函数散布东西，然后从 IO 使用这些纯函数。表达。更好的是尽可能将整个程序移出纯代码，以便可以独立评估除实际 I/O 之外的所有内容。只有当您需要由外部输入驱动的递归时，这才变得棘手，这让我想到最后一项:

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

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