From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.3 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 05C25BC0C for ; Thu, 1 Feb 2007 21:36:09 +0100 (CET) Received: from webmail4.sd.dreamhost.com (webmail4.sd.dreamhost.com [64.111.100.16]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l11Ka6wI027343 for ; Thu, 1 Feb 2007 21:36:08 +0100 Received: from webmail.fischerventure.com (localhost [127.0.0.1]) by webmail4.sd.dreamhost.com (Postfix) with ESMTP id 3BBA5302EF for ; Thu, 1 Feb 2007 12:35:59 -0800 (PST) Received: from 151.151.73.165 (SquirrelMail authenticated user robert@fischerventure.com) by webmail.fischerventure.com with HTTP; Thu, 1 Feb 2007 14:35:59 -0600 (CST) Message-ID: <54337.151.151.73.165.1170362159.squirrel@webmail.fischerventure.com> In-Reply-To: <17858.18833.95585.840472@serveur9-10.lri.fr> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <17858.18833.95585.840472@serveur9-10.lri.fr> Date: Thu, 1 Feb 2007 14:35:59 -0600 (CST) Subject: Re: [Caml-list] Programming with correctness guarantees From: "Robert Fischer" To: caml-list@inria.fr User-Agent: SquirrelMail/1.4.9a MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Miltered: at discorde with ID 45C24F36.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; arbitrarily:01 skipping:01 filliatre:01 oleg:01 beginner's:01 ocaml:01 bug:01 frightening:98 beginners:01 wrote:01 writes:01 writes:01 caml-list:01 caml-list:01 bin:01 What, exactly, is the difference between a unit test and formal verification of an application? I've long been under the opinion that Design-by-Contract is just a way to write unit tests quickly -- after all, you write something that looks kinda like code, attach it to something we arbitrarily define as a "unit", run some framework on that, and the framework tells you if something violates those rules. This sounds like unit testing to me. Now, I could be wrong, and there could be something obvious I'm missing, and I'd like to know if there is -- but it just doesn't seem like there's anything like a clear line between unit tests and program verification. Given that there isn't, it seems like people writing verified code aren't really skipping the unit testing phase at all: they're just doing unit testing in a funny way. ~~ Robert Fischer. Fischer Venture Management Corporation On Thu, February 1, 2007 2:12 pm, Jean-Christophe Filliatre wrote: > > Joshua D. Guttman writes: > > oleg@pobox.com writes: > > > > > I remember reading somewhere that after a division of > > > Siemens applied this technique to a high assurance > > > project, they noted an exhilarating feeling of being > > > able to program without unit tests. The code was correct > > > by construction. > > > > This seems really frightening. > > There's a joke around in the formal methods community: ``would you > prefer to get on a plane whose software has been proved correct or > has been tested?'' > > More seriously, I heard a similar remark from a French company which > formally verified the embedded code of an automatic subway line (using > the B method). They explained that, after the verification had been > completed, the unit phase was not suppressed, but greatly reduced. > > -- > Jean-Christophe > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >