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

[Goswin von Brederlow <goswin-v-b@web.de>]

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" <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).

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