当前位置：文江博客话题详情

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

发布于 2024-09-30 10:33:45 字数 1385 浏览 0 评论 0 原文

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

在提出上述问题并得到惊人的答复（谢谢大家！）后，我有决定缩小我的搜索范围，寻找一种可证明的、实用的 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”测试，并阅读原文问题 :-)

原文

Continuing on from ideas in: Are there any provable real-world languages?

I don't know about you, but I'm sick of writing code that I can't guarantee.

After asking the above question and getting a phenomenal response (Thanks all!) I have decided to narrow my search for a provable, pragmatic, approach to Haskell. I chose Haskell because it is actually useful (there are many web frameworks written for it, this seems a good benchmark) AND I think it is strict enough, functionally, that it might be provable, or at least allow the testing of invariants.

Here's what I want (and have been unable to find)

I want a framework that can look at a Haskell function, add, written in psudocode:

add(a, b):
    return a + b

- and check if certain invarients hold over every execution state. I'd prefer for some formal proof, however I would settle for something like a model-checker.
In this example, the invarient would be that given values a and b, the return value is always the sum a+b.

This is a simple example, but I don't think it is an impossibility for a framework like this to exist. There certainly would be an upper limit on the complexity of a function that could be tested (10 string inputs to a function would certainly take a long time!) but this would encourage more careful design of functions, and is no different than using other formal methods. Imagine using Z or B, when you define variables/sets, you make damn sure that you give the variables the smallest possible ranges. If your INT is never going to be above 100, make sure you initialise it as such! Techniques like these, and proper problem decomposition should - I think - allow for satisfactory checking of a pure-functional language like Haskell.

I am not - yet - very experienced with formal methods or Haskell. Let me know if my idea is a sound one, or maybe you think that haskell is not suited? If you suggest a different language, please make sure it passes the "has-a-web-framework" test, and do read the original question :-)

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

゛时过境迁 2024-10-07 10:33:45

好吧，既然你选择了 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 部分隔离为单个抽象函数，该函数易于理解并且通常不可避免地是正确的结合

Well, a few things to start with, since you're taking the Haskell route:

Are you familiar with the Curry-Howard correspondence? There are systems used for machine-checked proofs based on this which are, in many ways, simply functional programming languages with very powerful type systems.
Are you familiar with the areas of abstract mathematics that provide useful concepts for analyzing Haskell code? Various flavors of algebra and some bits of category theory come up a lot.
Keep in mind that Haskell, like all Turing-complete languages, always has the possibility of nontermination. In general, it's much harder to prove that something will always be true than it is to prove that either something will be true or will depend on a nonterminating value.

If you're seriously going for proof, not merely testing, these are the sort of things to keep in mind. The basic rule is this: Make invalid states cause compiler errors. Prevent invalid data from being encoded in the first place, then let the type checker do the tedious part for you.

If you want to go even further, if memory serves me the proof assistant Coq has an "extract to Haskell" feature that will let you prove arbitrary properties about critical functions, then turn the proofs into Haskell code.

For doing fancy type system stuff directly in Haskell, Oleg Kiselyov is the Grand Master. You can find examples on his site of neat tricks like higher-rank polymorphic types to encode static proofs of array bounds checking.

For more lightweight stuff, you can do things like using a type-level certificate to mark a piece of data as having been checked for correctness. You're still on your own for the correctness check itself, but other code can at least rely on knowing that some data has, in fact, been checked.

Another step you can take, building off of lightweight verification and fancy type system tricks, is to use the fact that Haskell works well as a host language for embedding domain-specific languages; first construct a carefully restricted sublanguage (ideally, one that isn't Turing-complete) about which you can more easily prove useful properties, then use programs in that DSL to provide key pieces of core functionality in your overall program. For instance, you could prove that a two-argument function is associative in order to justify parallelized reduction of a collection of items using that function (since the ordering of function application doesn't matter, only the ordering of arguments).

Oh, one last thing. Some advice on avoiding the pitfalls that Haskell does contain, which can sabotage code that would otherwise be safe-by-construction: Your sworn enemies here are general recursion, the IO monad, and partial functions:

The last is relatively easy to avoid: Don't write them, and don't use them. Make sure that every set of pattern matches handles every possible case, and never use error or undefined. The only tricky part is avoiding standard library functions that may cause errors. Some are obviously unsafe, like fromJust :: Maybe a -> a or head :: [a] -> a but others may be more subtle. If you find yourself writing a function that really, truly cannot do anything with some input values, then you're allowing invalid states to be encoded by the input type and need to fix that, first.
The second is easy to avoid on a superficial level by scattering stuff through assorted pure functions that are then used from an IO expression. Better is to, as much as possible, move the entire program out into pure code so that it can be evaluated independently with everything but the actual I/O. This mostly becomes tricky only when you need recursion that's driven by external input, which brings me to the final item:
Words to the wise: Well-founded recursion and productive corecursion. Always ensure that recursive functions are either going from some starting point to a known base case, or are generating a series of elements on demand. In pure code, the easiest way to do this is by either recursively collapsing a finite data structure (e.g., instead of a function calling itself directly while incrementing a counter up to some maximum, create a list holding the range of counter values and fold it) or recursively generating a lazy data structure (e.g. a list of progressive approximations to some value), while carefully never mixing the two directly (e.g., don't just "find the first element in the stream meeting some condition"; it might not exist. Instead, take values from the stream up to some maximum depth, then search the finite list, handling the not-found case appropriately).
Combining the last two items, for the parts where you really do need IO with general recursion, try to build the program as incremental components, then condense all the awkward bits into a single "driver" function. For instance, you could write a GUI event loop with a pure function like mainLoop :: UIState -> Events -> UIState, an exit test like quitMessage :: Events -> Bool, a function to get pending events getEvents :: IO Events, and an update function updateUI :: UIState -> IO (), then actually run the thing with a generalized function like runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO (). This keeps the complicated parts truly pure, letting you run the whole program with an event script and check the resulting UI state, while isolating the awkward recursive I/O parts into a single, abstract function that's easy to comprehend and will often be inevitably correct by parametricity.

回复收藏 0 原文

宣告ˉ结束 2024-10-07 10:33:45

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

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

回复收藏 0 原文

↙温凉少女 2024-10-07 10:33:45

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

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

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

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

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

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

I'm not sure whether what you ask for is actually what will make you happy. :-)

Model-checking a general purpose language is neigh impossible since models must be domain specific to be practical. Due to Gödel's Incompleteness Theorem, there simply is no method for automatically finding proofs in a sufficiently expressive logic.

This means that you have to write proofs yourself, which raises the question of whether the effort is worth the time spent. Of course, the effort creates something very valuable, namely the assurance that your program is correct. The question is not whether this is a must-have, but whether the time spent is too great a cost. The thing about proofs is that while you may have an "intuitive" understanding that your program is correct, it is often very difficult to formalize this understanding as a proof. The problem with intuitive understanding is that it's highly susceptible to accidental mistakes (typos and other stupid mistakes). This is the basic dilemma of writing correct programs.

So, research about program correctness is all about making it easier to formalize proofs and to check their correctness automatically. The programming is an integral part of the "ease of formalization"; it is very important to write programs in a style that is easy to reason about. Currently, we have the following spectrum:

Imperative language like C, C++, Fortran, Python: Very difficult to formalize anything here. Unit tests and general reasoning are the only way to get at least some assurance. Static typing catches only trivial bugs (which much better than not catching them!).
Purely functional languages like Haskell, ML: Expressive type system helps catch non-trivial bugs and mistakes. Proving correctness by hand is practical for snippets of up to somewhere around 200 lines, I'd say. (I did a proof for my operational package, for instance.) Quickcheck testing is a cheap substitute for formalized proofs.
Dependently typed languages and proof assistants like Agda, Epigram, Coq: Proving whole programs correct is possible thanks to automated help with proof formalization and discovery. However, the burden is still high.

In my opinion, the current sweet spot for writing correct programs is purely functional programming. If lives depend on the correctness of your program, you better go a level higher and use a proof assistant.

回复收藏 0 原文

冰火雁神 2024-10-07 10:33:45

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

回复收藏 0 原文

樱花细雨 2024-10-07 10:33:45

你看似简单的例子，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

Your seemingly simple example, add(a,b), is actually difficult to verify - floating point, overflow, underflow, interrupts, is the compiler verified, is the hardware verified, etc.

Habit is a simplified dialect of Haskell that allows for proving program properties.

Hume is a language with 5 levels, each more limitedand therefore easier to verify:

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

Of course, the most popular method today for proving program properties is unit testing, which provides strong theorems, but these theorems are overly specific. "Types Considered Harmful", Pierce, slide 66

回复收藏 0 原文

沉溺在你眼里的海 2024-10-07 10:33:45

看看 Zeno。引用维基页面：

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

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

回复收藏 0 原文

苍风燃霜 2024-10-07 10:33:45

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

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

回复收藏 0 原文

帥小哥 2024-10-07 10:33:45

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

回复收藏 0 原文

何以畏孤独 2024-10-07 10:33:45

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

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

回复收藏 0 原文

ˉ厌 2024-10-07 10:33:45

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