Haskell函数可以用正确性证明/模型检查/验证吗?

好吧,有几件事要开始,因为你走的是哈斯克尔路线:

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

• 您是否熟悉抽象数学中为分析Haskell代码提供有用概念的领域?各种各样的代数和一些范畴理论都出现了。

• 请记住,Haskell和所有图灵完整语言一样,总是有不终止的可能。一般来说,很难证明 要比证明某个东西是真的或依赖于一个非终止值更真实。

如果你真的想 ,不仅仅是 测试

如果你想走得更远,如果我有记忆的话 Coq 有一个“extract to 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

哦,最后一件事。关于避免Haskell所包含的陷阱的一些建议,这些陷阱可能会破坏本来可以通过构建安全的代码:这里是您的死敌 ,和 IO 单子 部分函数 :

• 最后一个相对容易避免:不要写,也不要用。确保每一组模式匹配处理每一个可能的情况,并且从不使用 error undefined . 唯一棘手的部分是避免使用可能导致错误的标准库函数。有些显然是不安全的,比如 fromJust :: Maybe a -> a 或 head :: [a] -> a

• 第二种方法在表面上很容易避免,它是将数据分散到各种纯函数中,然后从 输入输出

• 对智者说: 有根据的递归 和 . 始终确保递归函数不是从某个起点转到已知的基本情况,就是按需生成一系列元素。在纯代码中,最简单的方法是通过递归地折叠有限的数据结构(例如,而不是直接调用自己的函数,而将计数器递增到某个最大值),创建一个保持计数器值范围并折叠它的列表,或者递归地生成一个懒惰的数据结构(例如一个渐进的近似值列表),同时谨慎地从不直接混合这两个(例如,不要仅仅在流中找到满足某个条件的第一个元素”;它可能不存在。取而代之的是,将流中的值取到某个最大深度,然后搜索有限列表,适当处理未找到的情况)。

• 把最后两项结合起来,针对你真正需要的部分 输入输出 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 .

可能最接近你要求的是 Haskabelle ,一个随证明助手提供的工具 Isabelle 它可以把哈斯克尔的文件翻译成伊莎贝尔的理论,让你证明他们的东西。据我所知,这个工具是在HOL-ML-Haskell项目中开发的,并且 the documentation page 包含一些关于背后理论的信息。

Brian Huffman 一直在玩弄这些东西,看看他的文件和谈话,里面应该有相关的东西。

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

没有自动寻找证据的方法 以充分表达的逻辑。

自己校对 “直觉”地理解你的程序是正确的 很难将这种理解形式化 作为证据。直觉理解的问题是它很容易受到意外错误(打字错误和其他愚蠢的错误)的影响。这是编写正确程序的基本困境。

• 命令式语言,如C、C++、FORTRAN、Python:很难在这里实现任何形式化。单元测试和一般推理是至少获得一些保证的唯一方法。静态类型只捕获微不足道的错误(这比不捕获它们要好得多!).

• 纯粹的函数式语言,比如Haskell,ML:Expressive-type-system,有助于捕捉非平凡的bug和错误。手工证明正确性对于大约200行的片段来说是很实用的,我会说。(我为我的 operational package ,例如。) Quickcheck

• 依赖类型语言和证明助手,如Agda、Epigram、Coq:由于证明形式化和发现的自动化帮助,证明整个程序正确是可能的。但是,负担仍然很重。

在我看来,目前编写正确程序的最佳时机是 纯函数式编程 . 如果生命取决于你程序的正确性,你最好提高一个级别,并使用一个证明助手。

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

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

你看似简单的例子add(a,b)实际上很难验证——浮点、溢出、下溢、中断、编译器验证、硬件验证等等。

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

Hume 是一种有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

当然,现在最流行的证明程序属性的方法是单元测试,它提供了强大的定理,但是这些定理过于具体。 "Types Considered Harmful", Pierce, slide 66

看一看 Zeno . 引用wiki页面:

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

现在有许多程序验证工具都是模型检查工具,能够快速遍历非常大但有限的搜索空间。它们非常适合于具有大型描述但没有递归数据类型的问题。另一方面,Zeno被设计成在无限搜索空间上归纳证明性质,但仅限于那些具有小而简单规范的性质。

当然可以证明 一些 Haskell程序的性质。在我的FP考试中我不得不这样做:给出两个表达式,证明它们表示相同的函数。由于Haskell是图灵完备的,所以一般不可能做到这一点,所以任何机械证明都必须是一个证明助手(带用户指导的半自动)或模型检查器。

P-logic: property verification for Haskell programs 或 Proving the correctness of functional programs using Mizar . 两者都是学术论文,描述的方法多于实现。

http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

工具 AProVE 更多信息请参见 this paper ( shorter version ).

除此之外,你可能对 Dependent Types . 在这里,类型系统被扩展并用于使错误的程序不可能。

你可以用这个工具 hs-to-coq 要将Haskell大部分自动转换为Coq,然后使用Coq prove助手的全部功能来验证Haskell代码。看报纸 https://arxiv.org/abs/1803.06960 https://arxiv.org/abs/1711.09286 了解更多信息。