From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,834610f4f567e94b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.224.182.74 with SMTP id cb10mr13603975qab.0.1346836748205; Wed, 05 Sep 2012 02:19:08 -0700 (PDT) Received: by 10.236.152.5 with SMTP id c5mr2064123yhk.10.1346836748171; Wed, 05 Sep 2012 02:19:08 -0700 (PDT) Path: da15ni65566254qab.0!nntp.google.com!b19no2633545qas.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 5 Sep 2012 02:19:08 -0700 (PDT) In-Reply-To: <5045278b$0$6576$9b4e6d93@newsspool3.arcor-online.net> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=82.234.240.115; posting-account=IylMAAoAAAAOWceJ8n80VbFqxGquV1uU NNTP-Posting-Host: 82.234.240.115 References: <5045278b$0$6576$9b4e6d93@newsspool3.arcor-online.net> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <9f990735-e6ca-43b3-9be5-930e8184626a@googlegroups.com> Subject: Re: Hi-Lite high integrity showcase and overflow errors From: "yannick.moy" Injection-Date: Wed, 05 Sep 2012 09:19:08 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2012-09-05T02:19:08-07:00 List-Id: On Monday, September 3, 2012 11:56:28 PM UTC+2, Georg Bauhaus wrote: > http://www.open-do.org/projects/hi-lite/a-lighter-introduction-to-hi-lite= / > introduces AdaCore's new proof tools. This introduction makes me worry > about integrity, pardon me. This is a natural concern when considering formal verification technology. = As leader of the technical developments of GNATprove, I assure you that we = always have it in mind. And you are right on one thing: the code as presented in the "Light Introdu= ction to Hi-Lite" does not fly. This is confirmed by running GNATprove on y= our code: alicebob.adb:8:20: info: range check proved alicebob.adb:8:20: info: overflow check proved alicebob.adb:10:18: info: range check proved alicebob.adb:7:13: overflow check not proved Indeed, the possible overflow in line 7 (the test in Mult) can be raised at= run-time, hence the overflow check failure when compiling with -gnato. You can check these results by downloading GNATprove at http://www.open-do.= org/projects/hi-lite/gnatprove/ and running: $ gnatprove -P test --mode=3Dprove --report=3Dall (with a simple test.gpr project file setting the language to Ada 2012) > The high integrity example program fails miserably. (C programmers=20 > should have a good laugh.) You should take this example for what it is: an introduction to a research = project. When I wrote this example, GNATprove did not exist. Instead, I use= d Frama-C and SPARK (and I have given the corresponding annotations). With = these annotations, in particular the logical preconditions that X*Y<10000, = then you can prove that Mult is safe, and still call Mult in a context wher= e this precondition is not satisfied. One advantage of the new Ada 2012 exe= cutable annotations is that you can execute preconditions, which would catc= h the problem at the caller site. Now that a prototype for GNATprove is available, you can check that Mult is= indeed not safe as written. You can either add a precondition, or change M= y_Int definition into: subtype My_Int is Integer range 0 .. 10_000;=20 With this definition, GNATprove now proves all checks in Mult: alicebob.adb:8:20: info: range check proved alicebob.adb:8:20: info: overflow check proved alicebob.adb:10:18: info: range check proved alicebob.adb:7:13: info: overflow check proved I have modified the webpage to use this definition of Mult. Note that this = verification is dependent on the base type of Mult, so dependent on the tar= get for which you're doing the verification. That's a choice we have made f= or this technology, because we want to integrate proving and testing, and t= hat requires knowledge of target features. > So to ask a provocative question, what is the use of all these tools > if they still lead to programs that overflow so easily? They don't. > Or am I just incorrectly assuming thing and X * Y will make the tools > complain fiercely about possible overflow? Not fiercely, but in all cases where it cannot prove that it does not overf= low, it will issue an error message, yes.