可以Haskell职能证实/模型的检查/核实的正确性？

StackOverflow https://stackoverflow.com/questions/4077970

题

继续从思想中： 是否有任何可证明的真实世界的语言？

我不知道你怎么想，但是我 生病的编写代码，我不能保证。

后要求对上述问题，并得到一个惊人的响应(谢谢！) 我已经决定缩小我搜索了可证明的、务实的方法 Haskell.我选择了Haskell，因为它实际上是有用的(有 很多 网 框架 写的，这似乎是一个良好的基准) 和 我认为这是严格的足够的， 功能, ，它可能是可证明的，或者至少允许测试不变量。

这里就是我想要的 (并且一直无法找到)

我想要一个框架，可以看Haskell的功能，加，编写psudocode:

add(a, b):
    return a + b

-检查，如果某些invarients保持在每一个执行状态。我会更喜欢一些正式的证明，但是我会解决的东西就像一个模型的检查。
在这个例子中，invarient会，给出的数值 一个 和 b, 返回值总额 a+b.

这是一个简单的例子，但我不认为这是一个不可能为一个框架，这样的存在。那里肯定将是一个上限在复杂的功能，可以进行测试(10字符串输入功能无疑将需要很长的时间!) 但是，这将鼓励更多精心设计的功能，没有什么不同于用其他正式的方法。想象一下使用Z或B，当你变量的定义/套，你做该死的肯定，你得变量尽可能小的范围。如果你INT是永远不会超过100，确保初始化它作为这样的！技术这样的和适当的问题分解应该-我认为-允许令人满意的检查的一个纯粹的功能语言Haskell.

我不是-还没有-非常丰富的经验与正式的方法或Haskell.如果让我知道我的想法是一个合理的，或者，也许你认为haskell是不适合？如果你的建议不同的语言，请确保它通过的"具有一个网络的框架"测试，并阅读原始 的问题 :-)

有帮助吗？

解决方案

呃，一些事情的开始，因为你把Haskell路线：

  • 你熟悉的 咖喱-霍华德的对应关系?有系统的使用机器检查证据，在此基础上，在许多方面只是编程语言功能非常强大的类型的系统。

  • 你熟悉的领域的抽象的数学，提供了有用的概念，用于分析Haskell的代码？各种口味的代数和某些位的类别理论来了很多。

  • 请记住，Haskell，像所有的图灵完整的语言，总是有可能的nontermination.在一般情况下，这是很难证明的东西 总是 是真的不是要证明，无论是事情会是真实的或将取决于一个非终止的价值。

如果你真的要去 证明, 不仅仅是 测试, 这些是样的事情要牢记在心。基本规则是这样的：让无效的国家造成的编译错误。防止无效的数据编码在首位，然后让类型的检查程序不繁琐的一部分用于你。

如果你想更进一步，如果我证明助理 Coq 具有"中提取到Haskell"的功能，让你证明任意性质有关的关键职能，然后打开的证明成Haskell的代码。

这样做的花哨的类型系统的东西直接在Haskell， 奥列格*基谢廖夫是大师.你可以找到例子在他的网站的整洁的技巧喜欢 更高级的多晶型的编码静证据的阵列的边界检查.

为更轻型的东西，你可以做的事情一样 使用类型级别的证书 标记一块的数据为已经检查的正确性。你还在你自己的正确性检查本身，但其他代码至少可以依靠的了解的一些数据，事实上，已经进行检查。

另一个步骤可以采取建立轻核查和花哨的种类型的系统的技巧是使用的事实，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.

其他提示

可能是最接近您想要的东西 哈斯卡贝尔, ，带有证明助手的工具 伊莎贝尔 可以将Haskell文件转化为Isabelle理论，并让您证明有关它们的内容。据我了解，此工具是在HOL -ML- HASKELL项目中开发的 文档页面 包含有关背后理论的一些信息。

我对这个项目并不非常熟悉，我对此并不了解。但我知道 布莱恩·霍夫曼（Brian Huffman） 一直在玩这些事情，查看他的论文和谈话，它们应该包含相关内容。

我不确定您的要求是否实际上会让您开心。 :-)

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

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

因此，有关程序正确性的研究就是在使正式的证明和自动检查其正确性变得更加容易。该编程是“正式化易于性”的组成部分；以易于推理的方式编写程序非常重要。目前，我们有以下频谱：

  • 命令性语言，例如C，C ++，Fortran，Python：很难在这里形式化任何东西。单位测试和一般推理是至少获得一些保证的唯一方法。静态打字只会捕获琐碎的错误（这比不捕获它们要好得多！）。

  • 纯粹的功能性语言，例如Haskell，ML：表达类型系统有助于捕获非平凡的错误和错误。我想说，手工证明正确性是实用的，对于大约200行的大约200行的片段是实用的。 （我为我的证据做了证明 操作包, ， 例如。） 快速检查 测试是正式证明的廉价替代品。

  • 依赖性的类型语言和证明助手，例如AGDA，Epigram，Coq：证明整个程序正确，这要归功于自动化的正式化和发现的自动帮助。但是，负担仍然很高。

我认为，当前编写正确程序的最佳位置是 纯粹的功能编程. 。如果生活取决于您计划的正确性，则最好使用更高的水平并使用证明助手。

听起来您想要Esc/Haskell： http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm

哦，Agda现在确实有一个网络框架（至少是概念证明）： http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/

您看过Quickcheck吗？它可能会提供您需要的一些东西。

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

您看似简单的示例，添加（a，b）实际上很难验证 - 浮点，溢出，下流，中断，是对编译器验证的，是经过硬件验证的，等等。

习惯 是Haskell的简化方言，允许证明程序属性。

休ume 是一种具有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

看一下 zeno. 。引用Wiki页面：

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

当今可用的许多程序验证工具都是模型检查的多样性。能够迅速穿越非常大但有限的搜索空间。这些非常适合大量描述的问题，但没有递归数据类型。另一方面，ZENO旨在在无限搜索空间上诱导属性，但只有小规范的搜索空间。

当然有可能证明 一些 Haskell程序的属性正式。我必须在FP考试中这样做：给定两个表达式，证明它们表示相同的功能。由于Haskell是Turing-Complete，因此不可能做到这一点，因此任何机械供者都必须是证明助手（具有用户指导的半自动）或模型检查器。

朝这个方向进行了尝试，请参阅 P-Logic：Haskell程序的属性验证 或者 使用Mizar证明功能程序的正确性. 。两者都是描述方法的学术论文，而不是实施。

工具 抢劫 （至少）能够证明终止Haskell计划，这是证明正确性的一部分。可以在 这张纸 (较短的版本).

除此之外，您可能对 相关类型. 。在这里，类型系统被扩展并用来使错误程序不可能。

您可以使用该工具 hs-to-coq 要将haskell大多自动转换为COQ，然后使用Coq Prove Assisth的全部功能来验证您的Haskell代码。看到论文 https://arxiv.org/abs/1803.06960 和 https://arxiv.org/abs/1711.09286 有关更多信息。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top