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.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id B9CBEBC0B for ; Thu, 1 Feb 2007 21:57:31 +0100 (CET) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l11KvVjG003868 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Thu, 1 Feb 2007 21:57:31 +0100 Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id 1DDDE202167; Thu, 1 Feb 2007 21:57:31 +0100 (CET) Received: from serveur9-10.lri.fr (serveur9-10 [129.175.9.10]) by smtp.lri.fr (Postfix) with ESMTP id 44EE0CED98; Thu, 1 Feb 2007 21:57:28 +0100 (CET) Received: from filliatr by serveur9-10.lri.fr with local (Exim 3.36 #1 (Debian)) id 1HCizo-0005Fp-00; Thu, 01 Feb 2007 21:57:28 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <17858.21560.812318.17915@serveur9-10.lri.fr> Date: Thu, 1 Feb 2007 21:57:28 +0100 From: Jean-Christophe Filliatre To: "Robert Fischer" Cc: caml-list@inria.fr Subject: Re: [Caml-list] Programming with correctness guarantees In-Reply-To: <54337.151.151.73.165.1170362159.squirrel@webmail.fischerventure.com> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <17858.18833.95585.840472@serveur9-10.lri.fr> <54337.151.151.73.165.1170362159.squirrel@webmail.fischerventure.com> X-Mailer: VM 7.19 under Emacs 21.4.1 X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at concorde with ID 45C2543B.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 filliatr:01 lri:01 interprets:01 quantifiers:01 ocaml:01 forall:01 forall:01 writes:01 caml-list:01 incomplete:03 programming:03 unit:03 let:03 logical:04 Robert Fischer writes: > What, exactly, is the difference between a unit test and formal > verification of an application? (I hope I don't misunderstand what you mean by "formal verification" here) At least in its deductive form (i.e. frameworks similar to Hoare logic), formal verification interprets a program and its specification as a mathematical formula whose validity implies the program correctness. This formula usually includes universal quantifiers, and thus can only be proved using some logical reasoning, but not testing. If we consider for instance the following Ocaml code let min x y = if x <= y then x else y and the (incomplete) specification ``forall x y, min x y <= x'' then the correctness is equivalent to the following formula: forall x y, (x <= y implies x <= x) and (x > y implies y <= x) This is a statement easily established by most automatic provers. Then there is no need testing function min anymore, since it has been proved correct for _any_ input values. -- Jean-Christophe