This thread may be a good opportunity to advertize for some work on static program verification that has been applied to OCaml (sadly, it is actually quite rare to see program verification efforts for functional programming languages, in large part because funding bodies and reviewers appreciate applications to mainstream language with larger codebases). I am aware of the following, feel free to add more suggestions: - MoCHi http://www-kb.is.s.u-tokyo.ac.jp/~ryosuke/mochi/ Based on foundational work on model-checking of higher-order programs by Ong, Kobayashi and others (see the citations of the papers on the webpage), MoCHi can work with a subset of OCaml. It is not ready to handle real-world programs, both in term of verification time and the ocaml feature it understands, but going in the right direction -- and the underlying tools are rapidly improving, see e.g. the recent work on C-SHORe - Hybrid Contract Checking for OCaml, by Dana Xu http://gallium.inria.fr/~naxu/research/hcc.html (I previosuly mentioned on this list the available prototype that extends OCaml with dynamic contract checking) Another brand of work making good progress is the "Liquid Types" project in San Diego ( http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ ), which are working on applications to Haskell. Note that those tools are generally aimed at checking that programs respect some safety condition (eg. "does not end in an assertion failure"), not general specifications or general equivalence checking. You may consider encoding general equivalence checking in these term (traverse the input space and assert that the output of both functions are equivalent), but I don't know if the tools can handle the encoding efficiently. If you want full functional correctness for higher-order programs, rather than automated safety checkers, I would probably rather look at proof-assistant frameworks (eg. Ynot http://ynot.cs.harvard.edu/ or CFML http://www.chargueraud.org/softs/cfml/ ). On Mon, Sep 30, 2013 at 4:53 PM, Goswin von Brederlow wrote: > On Mon, Sep 30, 2013 at 08:26:46AM +0800, ?????? wrote: > > I dont think approach based on testing is a good solution, although I > have used it for a long time. > > This appraoch miss many conner case, which leads to error long after > modification and cost lots of time in debugging. > > Then your test suite was bad. You need enough tests to cover every > code path in your code and then some. Obviously in any complex code > you will forget / miss some. But over time your tests will improve too. > > > For the halting problem, I also dont think it can prevent us from > solving equivalent problem. Some undecidable problem, such as termination > checking, have been studied by bryon cook for a long time, and it can check > termination successfully for many programs. of course, it is not complete, > but most program written manually have some fixed pattern, not totally > random. > > > > for checking equivalent of ocaml program, most of my modification to my > program also have some fixed pattern, for example, using hash table > indexing to replace list searching. I think smt can solve it easily. May be > I need to solve it by my self? > > > > Shen > > > > > > > -----????????----- > > > ??????: "Florent Monnier" > > > ????????: 2013-09-30 00:19:29 (??????) > > > ??????: "??????" > > > ????: caml-list@inria.fr > > > ????: Re: [Caml-list] equivalent checking of ocaml program? > > > > > > 2013/09/29, Robert Jakob wrote: > > > > Well, the typical approach is to write a test suite before > refactoring > > > > and ensure that the test suite runs without errors before and after > the > > > > refactoring. > > > > > > > > To be sure that the program really behaves like before, you need to > > > > have a good (whatever this means) test suite. > > > > > > It may also be recommanded to keep the simple code next to the > optimised one. > > > It can be useful for many reasons. For example for the tests (compare > > > them), you can also use it as a failsafe alternative if the optimised > > > version fails. For the people who will try to read and understand your > > > code in the future (one of them might be you). > > I sometimes write a wrapper module around the code that runs both the > old and new code and compares the result. Only when both return the > same the value is returned. Run that with a large enough test suite or > simply use it for a while and you get good test coverage without > having to define input and output values. > > MfG > Goswin > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >