From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 0DC127EE4B for ; Mon, 30 Sep 2013 16:54:01 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=mailfrom; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am0CACqQSVLU4xEMlWdsb2JhbABav1GFPYEtFg4BAQEBBw0JCRIqgiUBAQQBOkQLCxgJJQ8FDRs0G4dYAQMJCrMnHysNiWqMZoJyFoMJgQMDlhaBaIYghiaIWg X-IPAS-Result: Am0CACqQSVLU4xEMlWdsb2JhbABav1GFPYEtFg4BAQEBBw0JCRIqgiUBAQQBOkQLCxgJJQ8FDRs0G4dYAQMJCrMnHysNiWqMZoJyFoMJgQMDlhaBaIYghiaIWg X-IronPort-AV: E=Sophos;i="4.90,1008,1371074400"; d="scan'208";a="34933558" Received: from mout.web.de ([212.227.17.12]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 30 Sep 2013 16:53:59 +0200 Received: from frosties.localnet ([95.208.119.3]) by smtp.web.de (mrweb004) with ESMTPSA (Nemesis) id 0MKNl8-1VSJY91iYY-001edf for ; Mon, 30 Sep 2013 16:53:59 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.80) (envelope-from ) id 1VQerG-0002Xt-QR for caml-list@inria.fr; Mon, 30 Sep 2013 16:53:58 +0200 Date: Mon, 30 Sep 2013 16:53:58 +0200 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20130930145358.GF8693@frosties> References: <37811b09.6ff.141695f3e3c.Coremail.syshen@nudt.edu.cn> <20130929165650.34da2e99@oberon> <1d5abd41.7b2.1416c429ca3.Coremail.syshen@nudt.edu.cn> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <1d5abd41.7b2.1416c429ca3.Coremail.syshen@nudt.edu.cn> User-Agent: Mutt/1.5.21 (2010-09-15) X-Provags-ID: V03:K0:OBZ5v9ALiteVdhb9q3Ea3xqnHSf0nZEhLs17i4FyIZDRGH7pY3S XqZSU/LvzpmP/RIUwJrvxPh/mJFNBnSlKjblVKypDjpg6cp9YVV37G+CQ1Ei4MV2rkkVQGU AmjL7Ia91zk/nsSvdP8wBQUd7ll92RBswU7a/AeiQSU2PryTJ+1hIEKUXukzX7SBykZchHh NOIakNolN/qvxKZvctAWQ== Subject: Re: [Caml-list] equivalent checking of ocaml program? 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