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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4847 bytes --]

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 <goswin-v-b@web.de>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" <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
>
> --
> 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
>

[-- Attachment #2: Type: text/html, Size: 6514 bytes --]