Re: [Caml-list] equivalent checking of ocaml program?

[沈胜宇 <syshen@nudt.edu.cn>]

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.

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" <monnier.florent@gmail.com>
> 发送时间: 2013-09-30 00:19:29 (星期一)
> 收件人: "沈胜宇" <syshen@nudt.edu.cn>
> 抄送: 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).
> 
> -- 
> bp.