Haskell函数可以证明/模型检查/验证是否具有正确性属性？ [英] Can Haskell functions be proved/model-checked/verified with correctness properties?

问题描述

继续观点：是否有任何可证明的现实世界语言？

我不了解你，但是我很厌烦写代码，我不能保证。

在询问了上述问题并获得了惊人的回复后（感谢所有！），我决定缩小搜索范围，以便采用可证实的实用方法来 Haskell 。我选择了Haskell，因为它确实有用（有很多 web 为它编写的框架，这似乎是一个很好的基准） AND 我认为它足够严格，功能上，它可能是可证明的，或者至少允许测试不变量。

这是我想要的（并且找不到）

我想要一个框架，可以查看Haskell函数，添加，写入psudocode中：

 添加（a，b）：
返回a + b 
  

- 并检查某些不变量坚持每一个执行状态。我更喜欢一些正式的证明，但是我会解决类似于模型检查器的问题。

在这个例子中，不变量是给定值 a 和 b ，返回值始终是总和 a + b 。

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

我还没有 - 非常有经验形式化方法或Haskell。让我知道我的想法是否合适，或者您认为haskell不适合？如果您建议使用不同的语言，请确保它通过has-a-web-framework测试，并阅读原始 question ： - ）

解决方案

开始的事情，因为你正在使用Haskell路由：

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

您是否熟悉抽象数学领域为分析Haskell代码提供了有用的概念？各种各样的代数和一些类别理论的味道出现了很多。请注意，与所有图灵完备语言一样，Haskell总有可能不终止。一般来说，要证明某些东西总是是真实的，而不是证明某些东西是真实的或者将取决于一个非终止值。

如果您认真考虑 proof ，而不仅仅是 ，那么这些都是要牢记。基本规则是：使无效状态导致编译器错误。防止无效数据首先被编码，然后让类型检查器为你做一些冗长的工作。

如果你想更进一步，如果内存服务于我证明助理 Coq 具有对Haskell的提取功能，可以让您证明关于关键的任意属性函数，然后将证明转换成Haskell代码。

为了直接在Haskell中做类似系统的东西，奥列格Kiselyov是大师。你可以在他的站点上找到例子，比如更高级的多态类型来编码静态的证明数组边界检查。

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

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

---

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

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

b $ b

• 第二种方法很容易避免在浅表级别通过分散各种各样的纯函数，然后通过 IO 表达式使用。更好的办法是尽可能将整个程序移出纯代码，以便除了实际的I / O之外的任何事情都可以独立评估。只有当你需要由外部输入驱动的递归时，这才会变得棘手，这会让我看到最后一项：

有效递归和生产性核心。始终确保递归函数要么从某个起点到已知的基本案例，要么正在按需生成一系列元素。在纯代码中，最简单的方法是通过递归折叠有限的数据结构（例如，而不是直接调用自己的函数，同时将计数器增加到某个最大值，创建一个包含计数器值范围并将其折叠的列表）或者递归地生成一个懒惰的数据结构（例如逐渐逼近某个值的列表），同时小心地不要直接混合这两个数据结构（例如，不要只是找到满足某种条件的流中的第一个元素;它可能不会存在，取而代之的是从流中取值到某个最大深度，然后搜索有限列表，适当地处理未找到的案例）。


• 结合最后两项，对于真正需要 IO 的部分进行一般递归，尝试将程序构建为增量组件，然后将所有不便的位压缩到单个驱动程序函数中。例如，你可以用一个纯函数来编写一个GUI事件循环，比如 mainLoop :: UIState - >活动 - > UIState ，退出测试，如 quitMessage :: Events - > Bool ，一个获取未决事件的函数 getEvents :: IO Events 和一个更新函数 updateUI :: UIState - > ; IO（），然后实际运行一个广义函数，如 runLoopIO ::（b - > a - > b） - > b - > IO a - > （b→IO（））→> IO（）。这使复杂的部分保持纯真，让您用事件脚本运行整个程序并检查生成的UI状态，同时将笨拙的递归I / O部分分离成单一的抽象函数，这些函数易于理解并且通常不可避免地是正确的通过 parametricity 。

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 :-)

解决方案

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.

这篇关于Haskell函数可以证明/模型检查/验证是否具有正确性属性？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！