From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 D965F7EE4B for ; Mon, 30 Sep 2013 02:34:15 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of syshen@nudt.edu.cn) identity=pra; client-ip=61.187.54.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="syshen@nudt.edu.cn"; x-sender="syshen@nudt.edu.cn"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of syshen@nudt.edu.cn) identity=mailfrom; client-ip=61.187.54.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="syshen@nudt.edu.cn"; x-sender="syshen@nudt.edu.cn"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@nudt.edu.cn) identity=helo; client-ip=61.187.54.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="syshen@nudt.edu.cn"; x-sender="postmaster@nudt.edu.cn"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsgMANfFSFI9uzYLY2dsb2JhbABahBGDKb0lKYE1AxgVBj6CJQEBBXkQBQQCGAQoAiE2BhMRCodZAw6OGZtQCIgODVeJE4Eli0GCODMHgmaBPAOJN4xfgWmMRYhlL4Fu X-IPAS-Result: AsgMANfFSFI9uzYLY2dsb2JhbABahBGDKb0lKYE1AxgVBj6CJQEBBXkQBQQCGAQoAiE2BhMRCodZAw6OGZtQCIgODVeJE4Eli0GCODMHgmaBPAOJN4xfgWmMRYhlL4Fu X-IronPort-AV: E=Sophos;i="4.90,1006,1371074400"; d="scan'208";a="28483141" Received: from mail.nudt.edu.cn (HELO nudt.edu.cn) ([61.187.54.11]) by mail3-smtp-sop.national.inria.fr with ESMTP; 30 Sep 2013 02:34:13 +0200 Received: by ajax-webmail-coremail.nudt.edu.cn (Coremail) ; Mon, 30 Sep 2013 08:26:46 +0800 (GMT+08:00) Date: Mon, 30 Sep 2013 08:26:46 +0800 (GMT+08:00) From: =?GBK?B?yfLKpNPu?= To: "Florent Monnier" Cc: caml-list@inria.fr Message-ID: <1d5abd41.7b2.1416c429ca3.Coremail.syshen@nudt.edu.cn> In-Reply-To: References: <37811b09.6ff.141695f3e3c.Coremail.syshen@nudt.edu.cn> <20130929165650.34da2e99@oberon> MIME-Version: 1.0 Content-Type: text/plain; charset=GBK Content-Transfer-Encoding: quoted-printable X-Originating-IP: [172.26.33.98] X-Priority: 3 X-Mailer: Coremail Webmail Server Version 4.0.5a build 20121109(20529.5019.5013) Copyright (c) 2002-2013 www.mailtech.cn nudt-out X-SendMailWithSms: false X-CM-TRANSID:AQAAf0AJOENHxUhSE70EAA--.484W X-CM-SenderInfo: xv1vxvnq6q3vvwohv3gofq/1tbiAQASE1C8UjsYbgAAsz X-Coremail-Antispam: 1Ur529EdanIXcx71UUUUU7IcSsGvfJ3iIAIbVAYjsxI4VWxJw CS07vEb4IE77IF4wCS07vE1I0E4x80FVAKz4kxMIAIbVAFxVCaYxvI4VCIwcAKzIAtYxBI daVFxhVjvjDU= Subject: Re: [Caml-list] equivalent checking of ocaml program? 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 modifi= cation and cost lots of time in debugging. For the halting problem, I also dont think it can prevent us from solving e= quivalent problem. Some undecidable problem, such as termination checking, = have been studied by bryon cook for a long time, and it can check terminati= on 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 pro= gram also have some fixed pattern, for example, using hash table indexing t= o replace list searching. I think smt can solve it easily. May be I need to= solve it by my self? Shen > -----=D4=AD=CA=BC=D3=CA=BC=FE----- > =B7=A2=BC=FE=C8=CB: "Florent Monnier" > =B7=A2=CB=CD=CA=B1=BC=E4: 2013-09-30 00:19:29 (=D0=C7=C6=DA=D2=BB) > =CA=D5=BC=FE=C8=CB: "=C9=F2=CA=A4=D3=EE" > =B3=AD=CB=CD: caml-list@inria.fr > =D6=F7=CC=E2: Re: [Caml-list] equivalent checking of ocaml program? >=20 > 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. >=20 > 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). >=20 > --=20 > bp.