0at*_*man 66 testing haskell formal-verification formal-methods functional-programming
继续观念:有没有可证明的现实世界语言？
我不了解你,但我厌倦了编写我无法保证的代码.
在询问了上述问题并得到了非凡的回应之后(谢谢大家!)我决定缩小我对Haskell的可证明,实用的方法的搜索范围.我选择哈斯克尔,因为它是真正有用的(也有许多 网页 框架为它写在纸上,这似乎是一个很好的基准)和我认为这是不够严格,在功能上,它可证明的,或者至少允许不变量的测试.
这就是我想要的(并且一直无法找到)
我想要一个可以查看Haskell函数的框架,添加,用psudocode编写:
add(a, b):
return a + b
- 并检查某些常量是否保持每个执行状态.我更喜欢一些正式的证据,但是我会满足于像模特检查员这样的东西.
在此示例中,不变量将是给定值a和b,返回值始终是总和a + b.
这是一个简单的例子,但我不认为这样的框架不可能存在.对于可以测试的函数的复杂性肯定会有一个上限(函数的10个字符串输入肯定会花费很长时间!)但这会鼓励更仔细地设计函数,并且与使用其他正式函数没有什么不同方法.想象一下,使用Z或B,当您定义变量/集时,您可以确保为变量提供尽可能小的范围.如果您的INT永远不会超过100,请确保将其初始化为!像这样的技术和正确的问题分解应该 - 我认为 - 允许对像Haskell这样的纯函数语言进行令人满意的检查.
我还没有 - 使用正式方法或Haskell非常有经验.让我知道我的想法是否合理,或者你认为haskell不合适？如果您建议使用其他语言,请确保通过"has-a-web-framework"测试,并阅读原始问题 :-)
C. *_*ann 60
好吧,有一些事情要开始,因为你正在采取Haskell路线:
你熟悉Curry-Howard的通信吗？有一些系统用于基于此的机器检查证明,在很多方面,它们只是功能强大的编程语言,具有非常强大的类型系统.
您是否熟悉抽象数学领域,为分析Haskell代码提供了有用的概念？各种各样的代数和一些类别理论都出现了很多.
请记住,Haskell与所有图灵完备语言一样,总是有可能无法终止.一般来说,要证明某些东西永远是真实的,要证明某事物是真的还是取决于非终结价值要困难得多.
如果你真的想要证明,而不仅仅是测试,那么这些都是要记住的事情.基本规则是:使无效状态导致编译器错误.首先防止无效数据被编码,然后让类型检查器为您完成繁琐的部分.
如果你想更进一步,如果内存为我提供证明助手,Coq有一个"提取到Haskell"功能,可以让你证明关键函数的任意属性,然后将证明转换成Haskell代码.
为了直接在Haskell中制作花哨型系统,Oleg Kiselyov是大师.你可以在他的网站上找到一些巧妙的技巧,例如更高级别的多态类型,以编码数组边界检查的静态证据.
对于更轻量级的东西,您可以执行诸如使用类型级证书将一段数据标记为已检查正确性的操作.您仍然可以自己进行正确性检查,但其他代码至少可以依赖于知道某些数据实际上已被检查过.
您可以采取的另一个步骤,即基于轻量级验证和花哨类型系统技巧,使用Haskell作为嵌入特定于域的语言的宿主语言的良好效果; 首先构建一个精心限制的子语言(理想情况下,不是图灵完备的),您可以更容易地证明其有用的属性,然后使用该DSL中的程序在整个程序中提供关键的核心功能.例如,您可以证明双参数函数是关联的,以证明使用该函数并行化减少项集合(因为函数应用程序的顺序无关紧要,只有参数的排序).
哦,最后一件事.关于避免Haskell确实包含的陷阱的一些建议,这可能会破坏原本可以安全构建的代码:这里的死敌是一般递归,IOmonad和部分函数:
最后一个相对容易避免:不要写它们,也不要使用它们.确保每组模式匹配都处理每种可能的情况,并且永远不要使用error或undefined.唯一棘手的部分是避免可能导致错误的标准库函数.有些人显然不安全,fromJust :: Maybe a -> a或者head :: [a] -> a其他人可能更加微妙.如果您发现自己编写的函数确实无法对某些输入值执行任何操作,那么您将允许无效状态由输入类型进行编码,并且需要先修复它.
通过各种纯函数分散东西,然后从IO表达式中使用,第二个很容易在表面上避免.更好的是尽可能地将整个程序移动到纯代码中,以便可以使用除实际I/O之外的所有内容独立地进行评估.只有当您需要由外部输入驱动的递归时,这才会变得棘手,这会将我带到最终项目:
明智的话:有根据的递归和富有成效的核心运动.始终确保递归函数从某个起始点到已知的基本情况,或者按需生成一系列元素.在纯代码中,最简单的方法是通过递归地折叠有限数据结构(例如,代替直接调用自身的函数,同时将计数器递增到某个最大值,创建一个包含计数器值范围的列表并折叠它)或者递归地生成一个惰性数据结构(例如,某些值的渐进近似列表),同时小心地不要直接混合两者(例如,不要只是"找到满足某些条件的流中的第一个元素";它可能不会相反,从流中取值到某个最大深度,然后搜索有限列表,适当地处理未找到的情况).
结合最后两项,对于您确实需要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部分隔离成一个易于理解的单个抽象函数,并且通常不可避免地是正确的通过参数化.
sve*_*son 20
可能与你要求的最接近的是Haskabelle,这是一个与证明助手Isabelle一起提供的工具,它可以将Haskell文件转换成Isabelle理论并让你证明它们的内容.据我所知,这个工具是在HOL - ML - Haskell项目中开发的,文档页面包含有关背后理论的一些信息.
我对这个项目并不十分熟悉,我不太了解它已经做了什么.但我知道Brian Huffman一直在玩这些东西,看看他的论文和谈话,他们应该包含相关的东西.
Hei*_*mus 18
我不确定你所要求的是否真的会让你开心.:-)
模型检查通用语言几乎是不可能的,因为模型必须是特定于领域的才能实用.由于哥德尔的不完备性定理,根本没有方法可以在充分表达的逻辑中自动查找证明.
这意味着你必须自己编写校样,这就提出了这个努力是否值得花费时间的问题.当然,这种努力创造了一些非常有价值的东西,即确保你的程序是正确的.问题不在于这是否是必须的,而是花费的时间是否太大.关于证明的事情是,虽然你可能对你的程序是正确的"直觉"理解,但通常很难将这种理解形式化为证明.直观理解的问题在于它极易受到意外错误(错别字和其他愚蠢错误)的影响.这是编写正确程序的基本困境.
因此,关于程序正确性的研究就是为了更容易地形式化证明并自动检查它们的正确性.编程是"易于形式化"的一个组成部分; 以易于推理的风格编写程序非常重要.目前,我们有以下频谱:
像C,C++,Fortran,Python这样的命令式语言:很难在这里形式化任何东西.单元测试和一般推理是获得至少一些保证的唯一方法.静态类型只捕获琐碎的错误(这比捕获它们要好得多!).
纯函数式语言,如Haskell,ML:Expressive类型系统有助于捕获非平凡的错误和错误.我会说,手工证明正确性对于大约200行的片段是切实可行的.(例如,我为我的操作包做了证明.)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/