From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <rj@robertjakob.de>
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 AF78A7EE4B
	for <caml-list@sympa.inria.fr>; Sun, 29 Sep 2013 16:56:53 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  rj@robertjakob.de) identity=pra; client-ip=37.59.40.50;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="rj@robertjakob.de";
  x-sender="rj@robertjakob.de"; x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  rj@robertjakob.de) identity=mailfrom; client-ip=37.59.40.50;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="rj@robertjakob.de";
  x-sender="rj@robertjakob.de"; x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@ks3000501.kimsufi.com) identity=helo;
  client-ip=37.59.40.50;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="rj@robertjakob.de";
  x-sender="postmaster@ks3000501.kimsufi.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgIHAC0+SFIlOygy/2dsb2JhbABZgwdGA4Nqr1UBiDyFOwqBFhZ0giUBAQQBI1YFCwkCGgIFIQICDy0bGYgACo1Lm1aSBxaBE44oBxYYgjyBOAOUOoNEkXqDJg
X-IPAS-Result: AgIHAC0+SFIlOygy/2dsb2JhbABZgwdGA4Nqr1UBiDyFOwqBFhZ0giUBAQQBI1YFCwkCGgIFIQICDy0bGYgACo1Lm1aSBxaBE44oBxYYgjyBOAOUOoNEkXqDJg
X-IronPort-AV: E=Sophos;i="4.90,1004,1371074400"; 
   d="scan'208";a="34790588"
Received: from ks3000501.kimsufi.com ([37.59.40.50])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 29 Sep 2013 16:56:52 +0200
Received: from oberon (dslb-088-064-168-128.pools.arcor-ip.net [88.64.168.128])
	by ks3000501.kimsufi.com (Postfix) with ESMTPSA id 67C16808AE;
	Sun, 29 Sep 2013 16:56:52 +0200 (CEST)
Date: Sun, 29 Sep 2013 16:56:50 +0200
From: Robert Jakob <rj@robertjakob.de>
To: caml-list@inria.fr
Cc: =?UTF-8?B?5rKI6IOc5a6H?= <syshen@nudt.edu.cn>
Message-ID: <20130929165650.34da2e99@oberon>
In-Reply-To: <37811b09.6ff.141695f3e3c.Coremail.syshen@nudt.edu.cn>
References: <37811b09.6ff.141695f3e3c.Coremail.syshen@nudt.edu.cn>
X-Mailer: Claws Mail 3.9.1 (GTK+ 2.24.13; x86_64-pc-linux-gnu)
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Subject: Re: [Caml-list] equivalent checking of ocaml program?

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.

And as others have mentioned, due to the Halting problem this can only
be an approximation in general.

r.

On Sun, 29 Sep 2013 18:59:11 +0800 (GMT+08:00)
=E6=B2=88=E8=83=9C=E5=AE=87 <syshen@nudt.edu.cn> wrote:

> Dear all:
>=20
>=20
> I am working hard to optimize my ocaml program, but I am not sure
> whether the significantly modified version is equal to the old
> version.
>=20
>=20
> So is there any research work on this topic?
>=20
>=20
> Shen
>=20