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,ab1d177a5a26577d X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!k10g2000vbn.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: SPARK and other provers (Was: Re: What's wrong with C++?) Date: Tue, 11 Oct 2011 02:40:58 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <1ee1a434-4048-48f6-9f5e-d8126bebb808@r19g2000prm.googlegroups.com> NNTP-Posting-Host: 88.97.49.112 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1318326955 17873 127.0.0.1 (11 Oct 2011 09:55:55 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 11 Oct 2011 09:55:55 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: k10g2000vbn.googlegroups.com; posting-host=88.97.49.112; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-Google-Web-Client: true X-Google-Header-Order: ARLUEHNKC X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:22336 Date: 2011-10-11T02:40:58-07:00 List-Id: On Oct 11, 8:45=A0am, Yannick Duch=EAne (Hibou57) wrote: > Le Mon, 10 Oct 2011 15:31:21 +0200, Paul Colin Gloster =A0 > a =E9crit: > > > Yannick Duch=EAne (Hibou57) sent on October = =A0 > > 9th, 2011: > > |-------------------------------------| > > |"[..] =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0| > > |[..] SPARK [..] and there is no ready| > > |accessible alternatives)." =A0 =A0 =A0 =A0 =A0 | > > |-------------------------------------| > > > There are many alternatives, but they lack built-in > > integration with Ada by default. > > Yes, it has too infer value ranges and other implicit validity conditions= =A0 > automatically, without explicit specifications from the author (will have= =A0 > a look at Alt-Ergo a future day, and an even farer future day, will have = =A0 > some personal experiments with something). > If you are considering using Alt-Ergo with SPARK you may be interested in this result from an experiment. Using some code that was already proved using the Simplifier (and which required a number of user rules) I let Alt-Ergo have a go at all the VCs that the Simplifer was unable to prove directly (i.e. without user rules). The first discovery was that the default proof steps limit (set to 5000 in GPS) is way too high (at least for my desktop - Core i5/750@2.67GHz). I had to bring it down to the 300-500 range. Secondly the Victor driver (the interface to Alt-Ergo) supplied with SPARK (and used by GPS) is very inflexible: - It enforces the option that all conclusions of a VC are 'fused' - so that failure to prove any one conclusion means that none of the conclusions are reported as proved - and there seems to be no way to find out which conclusion(s) are/are not provable. - There is no way for the user to supply any user rules to Alt-Ergo. This is essential if Alt-Ergo is going to have any chance of proving VCs that reference proof functions. (These restrictions can be easily worked round by some simple mods to the victor driver program.) Using the victor driver from the command line would also get round these problems, but the documentation provides no help with this. With these changes, the figures from the POGS summary are (omitting columns with all zeros): Total VCs by type: -----------Proved By Or Using----------- Total Spark Simp (User) ViCToR Assert/Post 118 0 100( 36) 18 Precondition 45 0 36( 3) 9 Check stmnt. 222 0 206( 154) 16 Runtime check 195 0 195 0 Refinem. VCs 6 5 1( 1) 0 Inherit. VCs 0 0 0 0 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D Totals: 586 5 538( 194) 43 %Totals: 1% 92%( 33%) 7% So Alt-Ergo completes the proof of 43 out of 237 VCs that are not directly proved by the Simplifier. That's one data point - does anyone else have any others? Cheers, Phil