blocks|key|3227377|text|你看过quickcheck了吗？它可能会提供一些你需要的东西。|type|unstyled|depth|inlineStyleRanges|entityRanges|data|3227378|http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck|offset|length|3227379|entityMap|0|LINK|mutability|MUTABLE|url^0|0|0|1P|0|0^^$0|@$1|2|3|4|5|6|7|M|8|@]|9|@]|A|$]]|$1|B|3|C|5|6|7|N|8|@]|9|@$D|O|E|P|1|Q]]|A|$]]|$1|F|3|-4|5|6|7|R|8|@]|9|@]|A|$]]]|G|$H|$5|I|J|K|A|$L|C]]]]

Have you had a look at quickcheck? It may offer some of the things you need.

<a href="http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck" rel="nofollow">http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck</a>

blocks|key|3013379|text|当然，可以正式地证明Haskell程序的一些性质。我必须在我的FP考试中这样做:给定两个表达式，证明它们表示相同的函数。这通常是不可能的，因为Haskell是Turing-complete的，所以任何机械验证者要么必须是验证助手(半自动的用户指导)，要么必须是模型检查器。|type|unstyled|depth|inlineStyleRanges|entityRanges|data|3013380|在这个方向上已经有一些尝试，例如P-logic:+property+verification+for+Haskell+programs或Proving+the+correctness+of+functional+programs+using+Mizar。两者都是描述方法而不是实现的学术论文。|offset|length|3013381|entityMap|0|LINK|mutability|MUTABLE|url|http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.3152|1|http://mizar.org/trybulec65/14.pdf^0|0|G|1F|0|1W|1M|1|0^^$0|@$1|2|3|4|5|6|7|P|8|@]|9|@]|A|$]]|$1|B|3|C|5|6|7|Q|8|@]|9|@$D|R|E|S|1|T]|$D|U|E|V|1|W]]|A|$]]|$1|F|3|-4|5|6|7|X|8|@]|9|@]|A|$]]]|G|$H|$5|I|J|K|A|$L|M]]|N|$5|I|J|K|A|$L|O]]]]

It's certainly possible to prove some properties of Haskell programs formally. I've had to do so at my FP exam: given two expressions, prove that they denote the same function. It's not possible to do this in general since Haskell is Turing-complete, so any mechanical prover would either have to be a proof assistant (semi-automatic with user guidance) or a model checker.

There have been attempts in this direction, see e.g. <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.3152" rel="nofollow">P-logic: property verification for Haskell programs</a> or <a href="http://mizar.org/trybulec65/14.pdf" rel="nofollow">Proving the correctness of functional programs using Mizar</a>. Both are academic papers describing methods more than implementations.

blocks|key|293116|text|好了，既然您采用的是Haskell路线，那么首先要做几件事：|type|unstyled|depth|inlineStyleRanges|entityRanges|data|293117|293118|你熟悉Curry-Howard+correspondence吗？在很多方面，这些系统都是简单的函数式编程语言，具有非常强大的类型系统。|unordered-list-item|offset|length|293119|你熟悉抽象数学领域，为分析Haskell代码提供有用的概念吗？各种不同风格的代数和一些范畴论出现了很多。|293120|请记住，与所有图灵完成语言一样，Haskell始终具有不终止的可能性。一般来说，证明某事总是真比证明某事将为真或依赖于非终结值要难得多。|293121|293122|如果你真的要去找证据，而不仅仅是测试，这些都是需要牢记的事情。基本规则是:使无效状态导致编译器错误。首先要防止对无效数据进行编码，然后让类型检查器为您完成繁琐的部分。|293123|如果你想走得更远，如果我没记错的话，证明助手Coq有一个“提取到Haskell”的功能，可以让你证明关于关键函数的任意性质，然后把证明转换成Haskell代码。|293124|直接在Haskell，Oleg+Kiselyov+is+the+Grand+Master中做花哨的类型系统工作。你可以在他的网站上找到像higher-rank+polymorphic+types+to+encode+static+proofs+of+array+bounds+checking这样的小把戏。|293125|对于更轻量级的东西，您可以执行诸如using+a+type-level+certificate之类的操作，将一段数据标记为已检查正确性。您仍然需要自己进行正确性检查，但其他代码至少可以依赖于知道某些数据实际上已经检查过了。|293126|在轻量级验证和花哨的类型系统技巧的基础上，您可以采取的另一个步骤是利用Haskell作为嵌入domain-specific+languages的宿主语言这一事实；首先构造一种仔细限制的子语言(理想情况下，子语言不是图灵完全的)，这样您可以更容易地证明有用的属性，然后使用该DSL中的程序在整个程序中提供核心功能的关键部分。例如，您可以证明一个双参数函数是相联的，以便证明使用该函数对项目集合进行并行缩减是合理的(因为函数应用程序的顺序并不重要，只有参数的顺序才重要)。|293127|293128|哦，最后一件事。关于避免Haskell确实包含的陷阱的一些建议，这些陷阱可能会破坏本来是通过构造来安全的代码:您在这里的死敌是monad通用递归函数、IO+和partial+functions。|style|BOLD|CODE|293129|293130|最后一个相对容易避免:不要编写它们，也不要使用它们。确保每一组匹配的模式都能处理所有可能的情况，并且永远不要使用error或undefined。唯一棘手的部分是避免可能导致错误的标准库函数。有些显然是不安全的，比如fromJust+::+Maybe+a+->+a或head+::+[a]+->+a，但其他的可能更微妙。如果您发现自己编写的函数确实不能对某些输入值做任何事情，那么您就会允许输入类型对无效状态进行编码，并且需要首先解决这个问题。|293131|第二个在表面上很容易避免，方法是将内容分散到各种纯函数中，然后从IO表达式中使用这些纯函数。更好的做法是，尽可能地将整个程序移到纯代码中，以便可以使用除实际I/O之外的所有内容对其进行独立评估。这主要是在需要由外部输入驱动的递归时才变得棘手，这将我带到最后一项：|293132|Words+to+the+wise：wise+be++productive+corecursion。始终确保递归函数要么从某个起始点到达已知的基本情况，要么按需生成一系列元素。在纯代码中，要做到这一点，最简单的方法是递归地折叠有限的数据结构(例如，当将计数器递增到某个最大值时，而不是直接调用函数本身，创建一个包含计数器值范围的列表并将其折叠)，或者递归地生成一个懒惰的数据结构(例如，对某个值进行渐进式近似的列表)，同时小心地从不直接混合这两个数据结构(例如，不要只是“在流中找到满足某些条件的第一个元素”；它可能不存在。取而代之的是，从流中获取最大深度的值，然后搜索有限列表，适当处理未找到的情况)。|293133|将最后两项结合起来，对于您确实需要使用常规递归的部分，尝试将程序构建为增量组件，然后将所有笨拙的部分压缩到一个“IO”函数中。例如，您可以使用纯函数(如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.|293134|通常不可避免地会纠正这个函数|293135|entityMap|0|LINK|mutability|MUTABLE|url|http://en.wikipedia.org/wiki/Curry%25E2%2580%2593Howard_correspondence|1|http://en.wikipedia.org/wiki/Coq|2|http://okmij.org/ftp/|3|http://okmij.org/ftp/Haskell/types.html#branding|4|http://lukepalmer.wordpress.com/2009/03/24/certificate-design-pattern/|5|http://en.wikipedia.org/wiki/Domain-specific_language|6|http://en.wikipedia.org/wiki/Parametricity^0|0|0|3|R|0|0|0|0|0|0|M|3|1|0|B|X|2|1W|26|3|0|H|U|4|0|1A|P|5|0|0|23|2|27|H|23|2|0|0|1K|5|1Q|9|2Z|O|3O|G|0|W|2|0|I|8|R|7N|0|0|B8|1K|2|24|14|3H|T|4M|M|5D|S|6T|1S|AU|D|6|0|0|E|0^^$0|@$1|2|3|4|5|6|7|1X|8|@]|9|@]|A|$]]|$1|B|3|-4|5|6|7|1Y|8|@]|9|@]|A|$]]|$1|C|3|D|5|E|7|1Z|8|@]|9|@$F|20|G|21|1|22]]|A|$]]|$1|H|3|I|5|E|7|23|8|@]|9|@]|A|$]]|$1|J|3|K|5|E|7|24|8|@]|9|@]|A|$]]|$1|L|3|-4|5|6|7|25|8|@]|9|@]|A|$]]|$1|M|3|N|5|6|7|26|8|@]|9|@]|A|$]]|$1|O|3|P|5|6|7|27|8|@]|9|@$F|28|G|29|1|2A]]|A|$]]|$1|Q|3|R|5|6|7|2B|8|@]|9|@$F|2C|G|2D|1|2E]|$F|2F|G|2G|1|2H]]|A|$]]|$1|S|3|T|5|6|7|2I|8|@]|9|@$F|2J|G|2K|1|2L]]|A|$]]|$1|U|3|V|5|6|7|2M|8|@]|9|@$F|2N|G|2O|1|2P]]|A|$]]|$1|W|3|-4|5|6|7|2Q|8|@]|9|@]|A|$]]|$1|X|3|Y|5|6|7|2R|8|@$F|2S|G|2T|Z|10]|$F|2U|G|2V|Z|10]|$F|2W|G|2X|Z|11]]|9|@]|A|$]]|$1|12|3|-4|5|6|7|2Y|8|@]|9|@]|A|$]]|$1|13|3|14|5|E|7|2Z|8|@$F|30|G|31|Z|11]|$F|32|G|33|Z|11]|$F|34|G|35|Z|11]|$F|36|G|37|Z|11]]|9|@]|A|$]]|$1|15|3|16|5|E|7|38|8|@$F|39|G|3A|Z|11]]|9|@]|A|$]]|$1|17|3|18|5|E|7|3B|8|@$F|3C|G|3D|Z|10]|$F|3E|G|3F|Z|10]]|9|@]|A|$]]|$1|19|3|1A|5|E|7|3G|8|@$F|3H|G|3I|Z|10]|$F|3J|G|3K|Z|11]|$F|3L|G|3M|Z|11]|$F|3N|G|3O|Z|11]|$F|3P|G|3Q|Z|11]|$F|3R|G|3S|Z|11]|$F|3T|G|3U|Z|11]]|9|@$F|3V|G|3W|1|3X]]|A|$]]|$1|1B|3|1C|5|6|7|3Y|8|@$F|3Z|G|40|Z|10]]|9|@]|A|$]]|$1|1D|3|-4|5|6|7|41|8|@]|9|@]|A|$]]]|1E|$1F|$5|1G|1H|1I|A|$1J|1K]]|1L|$5|1G|1H|1I|A|$1J|1M]]|1N|$5|1G|1H|1I|A|$1J|1O]]|1P|$5|1G|1H|1I|A|$1J|1Q]]|1R|$5|1G|1H|1I|A|$1J|1S]]|1T|$5|1G|1H|1I|A|$1J|1U]]|1V|$5|1G|1H|1I|A|$1J|1W]]]]

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

<ul>
<li>Are you familiar with the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="noreferrer">Curry-Howard correspondence</a>? 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.</li>
<li>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. </li>
<li>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.</li>
</ul>

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 <a href="http://en.wikipedia.org/wiki/Coq" rel="noreferrer">Coq</a> 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, <a href="http://okmij.org/ftp/" rel="noreferrer">Oleg Kiselyov is the Grand Master</a>. You can find examples on his site of neat tricks like <a href="http://okmij.org/ftp/Haskell/types.html#branding" rel="noreferrer">higher-rank polymorphic types to encode static proofs of array bounds checking</a>.

For more lightweight stuff, you can do things like <a href="http://lukepalmer.wordpress.com/2009/03/24/certificate-design-pattern/" rel="noreferrer">using a type-level certificate</a> 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 <a href="http://en.wikipedia.org/wiki/Domain-specific_language" rel="noreferrer">domain-specific languages</a>; 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).

<hr>

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 <code>IO</code> monad, and partial functions:

<ul>
<li>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 <code>error</code> or <code>undefined</code>. The only tricky part is avoiding standard library functions that may cause errors. Some are obviously unsafe, like <code>fromJust :: Maybe a -&gt; a</code> or <code>head :: [a] -&gt; a</code> 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.</li>
<li>The second is easy to avoid on a superficial level by scattering stuff through assorted pure functions that are then used from an <code>IO</code> 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:</li>
<li>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). </li>
<li>Combining the last two items, for the parts where you really do need <code>IO</code> 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 <code>mainLoop :: UIState -&gt; Events -&gt; UIState</code>, an exit test like <code>quitMessage :: Events -&gt; Bool</code>, a function to get pending events <code>getEvents :: IO Events</code>, and an update function <code>updateUI :: UIState -&gt; IO ()</code>, then actually run the thing with a generalized function like <code>runLoopIO :: (b -&gt; a -&gt; b) -&gt; b -&gt; IO a -&gt; (b -&gt; IO ()) -&gt; IO ()</code>. 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 <a href="http://en.wikipedia.org/wiki/Parametricity" rel="noreferrer">parametricity</a>.</li>
</ul>

blocks|key|290244|text|听起来你想要ESC/Haskell：http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm|type|unstyled|depth|inlineStyleRanges|entityRanges|offset|length|data|290245|哦，Agda现在确实有一个web框架(至少是概念验证)：http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/|290246|entityMap|0|LINK|mutability|MUTABLE|url|http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm|1|http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/^0|I|25|0|0|S|2A|1|0^^$0|@$1|2|3|4|5|6|7|P|8|@]|9|@$A|Q|B|R|1|S]]|C|$]]|$1|D|3|E|5|6|7|T|8|@]|9|@$A|U|B|V|1|W]]|C|$]]|$1|F|3|-4|5|6|7|X|8|@]|9|@]|C|$]]]|G|$H|$5|I|J|K|C|$L|M]]|N|$5|I|J|K|C|$L|O]]]]

Sounds like you want ESC/Haskell: <a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm" rel="noreferrer">http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm</a>

Oh, and Agda now does have a web framework (proof of concept, at least): <a href="http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/" rel="noreferrer">http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/</a>

blocks|key|3013485|text|我不确定你所要求的是否是真正能让你快乐的东西。:-)|type|unstyled|depth|inlineStyleRanges|entityRanges|data|3013486|通用语言的模型检查几乎是不可能的，因为模型必须是领域特定的才能实用。由于Gödel的不完全性定理，在一个充分表达的逻辑中，根本没有自动寻找证明的方法。|3013487|这意味着你必须自己写校样()，这就提出了这样一个问题:花这么多时间是否值得。当然，这种努力创造了一些非常有价值的东西，即确保你的程序是正确的。问题不是这是否是必需品，而是花费的时间是否太大。关于证明的事情是，虽然你可能对你的程序是正确的有一种“直观”的理解，但通常很难将这种理解形式化作为证明。直觉理解的问题是，它很容易发生意外错误(打字错误和其他愚蠢的错误)。这是编写正确程序的基本难题。|offset|length|style|BOLD|3013488|因此，对程序正确性的研究就是为了使证明更容易形式化并自动检查其正确性。编程是“易于形式化”的一个组成部分；以一种易于理解的风格编写程序是非常重要的。目前，我们有以下频谱：|3013489|3013490|命令式语言，如C，C%2B%2B，Fortran，Python:在这里很难形式化。单元测试和一般推理是获得至少一些保证的唯一方法。静态类型只捕获微小的bug(这比不捕获them!).|unordered-list-item|3013491|Purely函数式语言要好得多，例如Haskell，ML:+Expressive+type+system有助于捕获重要的bug和错误。我想说的是，手工证明正确性对于大约200行左右的代码片段是可行的。(例如，我为我的operational+package做了一个证明)+Quickcheck测试是形式化的proofs.|3013492|Dependently类型语言和证明助手的廉价替代品，如Agda、Epigram、Coq:由于证明形式化和发现的自动化帮助，证明整个程序是可能的。然而，负担仍然很高。|3013493|3013494|在我看来，目前编写正确程序的最佳时机是纯函数式编程。如果生命依赖于你的程序的正确性，你最好更上一层楼，使用一个证明助手。|3013495|entityMap|0|LINK|mutability|MUTABLE|url|http://projects.haskell.org/operational/|1|http://book.realworldhaskell.org/read/testing-and-quality-assurance.html^0|0|0|3D|22|0|0|2D|0|0|0|2F|0|0|4F|30|J|0|3R|A|1|0|0|2B|0|0|0|1O|0^^$0|@$1|2|3|4|5|6|7|16|8|@]|9|@]|A|$]]|$1|B|3|C|5|6|7|17|8|@]|9|@]|A|$]]|$1|D|3|E|5|6|7|18|8|@$F|19|G|1A|H|I]]|9|@]|A|$]]|$1|J|3|K|5|6|7|1B|8|@$F|1C|G|1D|H|I]]|9|@]|A|$]]|$1|L|3|-4|5|6|7|1E|8|@]|9|@]|A|$]]|$1|M|3|N|5|O|7|1F|8|@$F|1G|G|1H|H|I]]|9|@]|A|$]]|$1|P|3|Q|5|O|7|1I|8|@$F|1J|G|1K|H|I]]|9|@$F|1L|G|1M|1|1N]|$F|1O|G|1P|1|1Q]]|A|$]]|$1|R|3|S|5|O|7|1R|8|@$F|1S|G|1T|H|I]]|9|@]|A|$]]|$1|T|3|-4|5|6|7|1U|8|@]|9|@]|A|$]]|$1|U|3|V|5|6|7|1V|8|@$F|1W|G|1X|H|I]]|9|@]|A|$]]|$1|W|3|-4|5|6|7|1Y|8|@]|9|@]|A|$]]]|X|$Y|$5|Z|10|11|A|$12|13]]|14|$5|Z|10|11|A|$12|15]]]]

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:

<ul>
<li>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!).</li>
<li>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 <a href="http://projects.haskell.org/operational/" rel="noreferrer">operational package</a>, for instance.) <a href="http://book.realworldhaskell.org/read/testing-and-quality-assurance.html" rel="noreferrer">Quickcheck</a> testing is a cheap substitute for formalized proofs.</li>
<li>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.</li>
</ul>

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.

blocks|key|293149|text|可能最接近你所要求的是Haskabelle，这是一个带有证明助手Isabelle的工具，它可以将哈斯克尔文件翻译成伊莎贝尔理论，并让你证明他们的东西。据我所知，这个工具是在HOL+-+ML+-+Haskell项目中开发的，the+documentation+page包含了一些关于背后理论的信息。|type|unstyled|depth|inlineStyleRanges|entityRanges|offset|length|data|293150|我对这个项目不是很熟悉，也不太了解它做了什么。但我知道Brian+Huffman一直在玩弄这些东西，看看他的论文和演讲，它们应该包含相关的东西。|293151|entityMap|0|LINK|mutability|MUTABLE|url|http://isabelle.in.tum.de/website-Isabelle2009/haskabelle.html|1|http://isabelle.in.tum.de/website-Isabelle2009/index.html|2|http://isabelle.in.tum.de/website-Isabelle2009/documentation.html|3|http://www21.in.tum.de/~huffman/^0|B|A|0|W|8|1|33|M|2|0|R|D|3|0^^$0|@$1|2|3|4|5|6|7|T|8|@]|9|@$A|U|B|V|1|W]|$A|X|B|Y|1|Z]|$A|10|B|11|1|12]]|C|$]]|$1|D|3|E|5|6|7|13|8|@]|9|@$A|14|B|15|1|16]]|C|$]]|$1|F|3|-4|5|6|7|17|8|@]|9|@]|C|$]]]|G|$H|$5|I|J|K|C|$L|M]]|N|$5|I|J|K|C|$L|O]]|P|$5|I|J|K|C|$L|Q]]|R|$5|I|J|K|C|$L|S]]]]

Probably the closest thing to what you're asking for is <a href="http://isabelle.in.tum.de/website-Isabelle2009/haskabelle.html" rel="nofollow noreferrer">Haskabelle</a>, a tool that comes with the proof assistant <a href="http://isabelle.in.tum.de/website-Isabelle2009/index.html" rel="nofollow noreferrer">Isabelle</a> which can translate Haskell files into Isabelle theories and lets you prove stuff about them. As far as I understand this tool is developed within the HOL - ML - Haskell project and <a href="http://isabelle.in.tum.de/website-Isabelle2009/documentation.html" rel="nofollow noreferrer">the documentation page</a> contains some information about the theory behind.

I'm not terribly familiar with this project and I don't know very much about what has been done with it. But I know <a href="http://www21.in.tum.de/~huffman/" rel="nofollow noreferrer">Brian Huffman</a> has been playing around with these things, check out his papers and talks, they should contain relevant stuff.

blocks|key|292416|text|MSR剑桥的一些最新努力：http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf|type|unstyled|depth|inlineStyleRanges|entityRanges|offset|length|data|292417|entityMap|0|LINK|mutability|MUTABLE|url|http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf^0|D|28|0|0^^$0|@$1|2|3|4|5|6|7|L|8|@]|9|@$A|M|B|N|1|O]]|C|$]]|$1|D|3|-4|5|6|7|P|8|@]|9|@]|C|$]]]|E|$F|$5|G|H|I|C|$J|K]]]]

Some very recent effort by MSR Cambridge:
<a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf" rel="nofollow">http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf</a>

blocks|key|293155|text|工具AProVE+(至少)能够证明Haskell程序的终止，这是证明正确性的一部分。有关更多信息，请访问this+paper+(shorter+version)。|type|unstyled|depth|inlineStyleRanges|entityRanges|offset|length|data|293156|除此之外，您可能会对Dependent+Types感兴趣。在这里，类型系统被扩展并被用来使错误的程序不可能。|293157|entityMap|0|LINK|mutability|MUTABLE|url|http://aprove.informatik.rwth-aachen.de/|1|http://dl.acm.org/citation.cfm?doid=1890028.1890030|2|http://verify.rwth-aachen.de/giesl/papers/RTA06-distribute.ps|3|http://www.haskell.org/haskellwiki/Dependent_type^0|2|6|0|1G|A|1|1S|F|2|0|A|F|3|0^^$0|@$1|2|3|4|5|6|7|T|8|@]|9|@$A|U|B|V|1|W]|$A|X|B|Y|1|Z]|$A|10|B|11|1|12]]|C|$]]|$1|D|3|E|5|6|7|13|8|@]|9|@$A|14|B|15|1|16]]|C|$]]|$1|F|3|-4|5|6|7|17|8|@]|9|@]|C|$]]]|G|$H|$5|I|J|K|C|$L|M]]|N|$5|I|J|K|C|$L|O]]|P|$5|I|J|K|C|$L|Q]]|R|$5|I|J|K|C|$L|S]]]]

The tool <a href="http://aprove.informatik.rwth-aachen.de" rel="nofollow">AProVE</a> is (at least) able to prove termination of Haskell programs, which is part of proving correctness.
More information can be found in <a href="http://dl.acm.org/citation.cfm?doid=1890028.1890030" rel="nofollow">this paper</a> (<a href="http://verify.rwth-aachen.de/giesl/papers/RTA06-distribute.ps" rel="nofollow">shorter version</a>).

Apart from that, you might be interested in <a href="http://www.haskell.org/haskellwiki/Dependent_type" rel="nofollow">Dependent Types</a>. Here, the type system is extended and used to make wrong programs impossible.

blocks|key|3013522|text|看看Zeno吧。引用维基页面：|type|unstyled|depth|inlineStyleRanges|entityRanges|offset|length|data|3013523|Haskell+Zeno是|3013524|程序属性的自动证明系统；由伦敦帝国理工学院威廉·索尼克斯、索菲娅·德罗索普鲁和苏珊·艾森巴赫开发。它旨在解决任何输入值的两个Haskell项之间相等的一般问题。|blockquote|3013525|3013526|今天可用的许多程序验证工具都是模型检查的变体；能够非常快速地遍历非常大但有限的搜索空间。它们非常适合于具有大量描述但没有递归数据类型的问题。另一方面，Zeno被设计用于归纳地证明无限搜索空间上的性质，但仅限于那些具有小而简单的规范的性质。|3013527|entityMap|0|LINK|mutability|MUTABLE|url|http://www.haskell.org/haskellwiki/Zeno^0|2|4|0|0|0|0|0|0^^$0|@$1|2|3|4|5|6|7|T|8|@]|9|@$A|U|B|V|1|W]]|C|$]]|$1|D|3|E|5|6|7|X|8|@]|9|@]|C|$]]|$1|F|3|G|5|H|7|Y|8|@]|9|@]|C|$]]|$1|I|3|-4|5|6|7|Z|8|@]|9|@]|C|$]]|$1|J|3|K|5|6|7|10|8|@]|9|@]|C|$]]|$1|L|3|-4|5|6|7|11|8|@]|9|@]|C|$]]]|M|$N|$5|O|P|Q|C|$R|S]]]]

Have a look at <a href="http://www.haskell.org/haskellwiki/Zeno" rel="nofollow">Zeno</a>. Quoting the wiki page:

<blockquote>
 Zeno is an automated proof system for Haskell program properties; developed at Imperial College London by William Sonnex, Sophia Drossopoulou and Susan Eisenbach. It aims to solve the general problem of equality between two Haskell terms, for any input value.
 
 Many program verification tools available today are of the model checking variety; able to traverse a very large but finite search space very quickly. These are well suited to problems with a large description, but no recursive datatypes. Zeno on the other hand is designed to inductively prove properties over an infinite search space, but only those with a small and simple specification. 
</blockquote>

blocks|key|292439|text|您可以使用工具hs-to-coq将Haskell基本上自动转换为Coq，然后使用Coq+prove助手的全部功能来验证您的Haskell代码。有关更多信息，请参阅论文https://arxiv.org/abs/1803.06960和https://arxiv.org/abs/1711.09286。|type|unstyled|depth|inlineStyleRanges|offset|length|style|CODE|entityRanges|data|292440|entityMap|0|LINK|mutability|MUTABLE|url|https://github.com/antalsz/hs-to-coq/|1|https://arxiv.org/abs/1803.06960|2|https://arxiv.org/abs/1711.09286^0|7|9|7|9|0|2B|W|1|38|W|2|0^^$0|@$1|2|3|4|5|6|7|R|8|@$9|S|A|T|B|C]]|D|@$9|U|A|V|1|W]|$9|X|A|Y|1|Z]|$9|10|A|11|1|12]]|E|$]]|$1|F|3|-4|5|6|7|13|8|@]|D|@]|E|$]]]|G|$H|$5|I|J|K|E|$L|M]]|N|$5|I|J|K|E|$L|O]]|P|$5|I|J|K|E|$L|Q]]]]

You can use the tool <a href="https://github.com/antalsz/hs-to-coq/" rel="nofollow noreferrer"><code>hs-to-coq</code></a> to convert Haskell mostly automatic into Coq, and then use the full power of the Coq prove assistant to verify your Haskell code. See the papers <a href="https://arxiv.org/abs/1803.06960" rel="nofollow noreferrer">https://arxiv.org/abs/1803.06960</a> and <a href="https://arxiv.org/abs/1711.09286" rel="nofollow noreferrer">https://arxiv.org/abs/1711.09286</a> for some more information.

Continuing on from ideas in: <a href="https://stackoverflow.com/questions/4065001/are-there-any-provable-real-world-languages-scala">Are there any provable real-world languages?</a>

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 <a href="http://www.haskell.org/" rel="noreferrer">Haskell</a>. I chose Haskell because it is actually useful (there are <a href="http://snapframework.com/" rel="noreferrer">many</a> <a href="http://happstack.com/" rel="noreferrer">web</a> <a href="http://www.turbinado.org/" rel="noreferrer">frameworks</a> written for it, this seems a good benchmark) AND I think it is strict enough, <a href="http://en.wikipedia.org/wiki/Functional_programming" rel="noreferrer">functionally</a>, 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:

<pre><code>add(a, b):
 return a + b
</code></pre>

- 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 <a href="https://stackoverflow.com/questions/4065001/are-there-any-provable-real-world-languages-scala">question</a> :-)

Can Haskell functions be proved/model-checked/verified with correctness properties?

翻译质量差，导致语言生硬或混乱。

没有提供实际的解决方法或示例。

解答不清晰，无法理解或解决问题。

页面排版不美观，阅读体验差。

文章

问答

视频

学习中心

腾讯云实验室

直播

竞赛

腾讯云代码分析专区

腾讯iOA零信任安全管理系统专区

腾讯云架构师技术同盟交流圈

腾讯云数据库专区

腾讯云顾问专区

腾讯云原生专区

腾讯混元专区

腾讯云TCE专区

腾讯云Lighthouse专区

腾讯云HAI专区

腾讯云Edgeone专区

腾讯云存储专区

腾讯云智能专区

腾讯轻联专区 

腾讯云开发专区

TAPD专区

腾讯轻量云游戏服专区

腾讯云最具价值专家

腾讯云架构师技术同盟

腾讯云创作之星

腾讯云开发者先锋

腾讯云代码助手

云原生构建

TAPD 敏捷项目管理

Cloud Studio

SDK中心

API中心

命令行工具

涵盖代码开发、场景应用、自动测试全流程，助你从零构建专属AI助手

一站式MCP教程库，解锁AI应用新玩法

从中的想法继续：我不知道你是怎么想的，但是我已经厌倦了写那些我不能保证的代码。在问了上面的问题并得到了惊人的回应之后(谢谢大家！)我决定缩小我的搜索范围，寻找一种可证明的、实用的方法。我选择Haskell是因为它实际上很有用(有为它编写的  ，这似乎是一个很好的基准测试)和我认为它足够严格，，它可能是可证明的，或者至少...

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

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

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

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

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