From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 44AFA7EE4C for ; Mon, 30 Sep 2013 17:49:54 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.44 as permitted sender) identity=mailfrom; client-ip=209.85.214.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f44.google.com) identity=helo; client-ip=209.85.214.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f44.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At8BAEqdSVLRVdYsm2dsb2JhbABaFoMpUq4lihSIRIElCBYOAQEBAQEGCwsJFCiCJQEBBAFAARsSCwEDAQsGBQsNDSEhAQERAQUBChIGEwkJCYdYAQMJBgyfN4xSgwqEFQoZJwMKFU+JAAEFDIxaGYJOBAeEIgOUIoF0gWmBL4sWg0oYKYRPOg X-IPAS-Result: At8BAEqdSVLRVdYsm2dsb2JhbABaFoMpUq4lihSIRIElCBYOAQEBAQEGCwsJFCiCJQEBBAFAARsSCwEDAQsGBQsNDSEhAQERAQUBChIGEwkJCYdYAQMJBgyfN4xSgwqEFQoZJwMKFU+JAAEFDIxaGYJOBAeEIgOUIoF0gWmBL4sWg0oYKYRPOg X-IronPort-AV: E=Sophos;i="4.90,1008,1371074400"; d="scan'208";a="28584508" Received: from mail-bk0-f44.google.com ([209.85.214.44]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 30 Sep 2013 17:49:53 +0200 Received: by mail-bk0-f44.google.com with SMTP id mz10so2153462bkb.3 for ; Mon, 30 Sep 2013 08:49:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=Fy1AqwhxLN4IWT47Gu+Z1uLBxwFbDVljbKD7DUpDnAQ=; b=a/LgRprtorEZUsDoNZPn5rPiJusggLsKA/Nm0fI1/bDO06dKyUi4iyxq14Z1pdzOrI Y7hS9O5xlIwq23Tn01uZSODHFp6JKytNrKAQA+wYHN9ZDR+lHk/0wYbRhFrh8ZhGVTy/ 9LHtUFPGOMFet7nNraizoinJLfuT8+eEd+uV6Z5iYMi/9T4PBjfi2GCGuZLKh0rSqyDw cFHPvCPfYZDmif+PVzkzUp10RwlSKKy2bzM6z5+5rh/e66blhAVLVzJ4648uxlATMz1p jf2QkxN7rCmTY86c8d4t04vvcTZ6znV8M8Y2SvADbVLrXvV2s5+LCcvvv7+gJL3d+GKO p/wg== X-Received: by 10.204.227.140 with SMTP id ja12mr2428696bkb.29.1380556191802; Mon, 30 Sep 2013 08:49:51 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.236.193 with HTTP; Mon, 30 Sep 2013 08:49:11 -0700 (PDT) In-Reply-To: <20130930145358.GF8693@frosties> References: <37811b09.6ff.141695f3e3c.Coremail.syshen@nudt.edu.cn> <20130929165650.34da2e99@oberon> <1d5abd41.7b2.1416c429ca3.Coremail.syshen@nudt.edu.cn> <20130930145358.GF8693@frosties> From: Gabriel Scherer Date: Mon, 30 Sep 2013 17:49:11 +0200 Message-ID: To: Goswin von Brederlow Cc: caml users Content-Type: multipart/alternative; boundary=485b3970d29067eb8e04e79bc926 Subject: Re: [Caml-list] equivalent checking of ocaml program? --485b3970d29067eb8e04e79bc926 Content-Type: text/plain; charset=ISO-8859-1 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 > --485b3970d29067eb8e04e79bc926 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
This thread may be a good op= portunity to advertize for some work on static program verification that ha= s been applied to OCaml (sadly, it is actually quite rare to see program ve= rification efforts for functional programming languages, in large part beca= use funding bodies and reviewers appreciate applications to mainstream lang= uage 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/
=A0 Based on = foundational work on model-checking of higher-order programs by Ong, Kobaya= shi 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, bu= t going in the right direction -- and the underlying tools are rapidly impr= oving, see e.g. the recent work on C-SHORe
- Hybrid Contract Checking for OCaml, by Dana Xu http://gallium.inria.fr/~naxu/resea= rch/hcc.html
=A0 (I previosuly mentioned on this list the avai= lable prototype that extends OCaml with dynamic contract checking)

Another brand of work making good progress is the "Liquid Ty= pes" 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 progra= ms respect some safety condition (eg. "does not end in an assertion fa= ilure"), not general specifications or general equivalence checking. Y= ou may consider encoding general equivalence checking in these term (traver= se the input space and assert that the output of both functions are equival= ent), 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-assi= stant frameworks (eg. Ynot http://y= not.cs.harvard.edu/ or CFML http://www.chargueraud.org/softs/cfml/ ).

<= /div>


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 m= odification 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 solv= ing equivalent problem. Some undecidable problem, such as termination check= ing, have been studied by bryon cook for a long time, and it can check term= ination successfully for many programs. of course, it is not complete, but = most program written manually have some fixed pattern, not totally random.<= br> >
> for checking equivalent of ocaml program, most of my modification to m= y program also have some fixed pattern, for example, using hash table index= ing to replace list searching. I think smt can solve it easily. May be I ne= ed 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 r= efactoring
> > > and ensure that the test suite runs without errors before an= d 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 op= timised one.
> > It can be useful for many reasons. For example for the tests (com= pare
> > them), you can also use it as a failsafe alternative if the optim= ised
> > 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
=A0 =A0 =A0 =A0 Goswin

--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://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

--485b3970d29067eb8e04e79bc926--