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: 103376,45ec8ce891c0398e,start X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!p12g2000vbo.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: SPARK: Defining the meaning of a proof function Date: Sun, 27 Feb 2011 04:51:42 -0800 (PST) Organization: http://groups.google.com Message-ID: <39202e76-0c9e-4e10-926b-1305fe818e01@p12g2000vbo.googlegroups.com> NNTP-Posting-Host: 88.97.49.112 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: posting.google.com 1298811103 12909 127.0.0.1 (27 Feb 2011 12:51:43 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 27 Feb 2011 12:51:43 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: p12g2000vbo.googlegroups.com; posting-host=88.97.49.112; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 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:18595 Date: 2011-02-27T04:51:42-08:00 List-Id: One significant gap in the SPARK language is the absence of any way to define the meaning of a proof function (i.e. a function declared in annotations). The only way to do this is in a user proof rule that is read by the Simplifier. If the user were able to define the meaning of a proof function in the SPARK text then this could be incorporated into the VCs generated by the Examiner. This would remove the need for a number of user rules and make completion of the proofs simpler, quicker and less error- prone. At present, a function operation can be given a return annotation, and this is used to add a hypothesis about the value returned by a call of that function - but only where that operation appears in code. Hypotheses are not added when the equivalent proof function appears in a proof context (pre/post, assert, check). As an experiment I extended my SPARKRules utility to mimic the effect of adding proof function definitions to SPARK. The extended program edits the Examiner generated VCs to add the hypotheses that (I think) the Examiner would add if it had definitions for proof functions. The results were very positive and suggest that the combination of adding proof function definitions to SPARK and using more capable solvers via Victor has the potential to make proof a great deal simpler and quicker. I used the current version of the Tokeneer software as the trial application. Full details of the work and the results are in: http://www.sparksure.com/resources/Proof_Function_Definitions.pdf Summarising the results: * The current version of Tokeneer has 84 distinct user rules (some very complex) that create 97 rules in 26 user rule files. These complete the proofs of 101 VCs in 43 operations. (There are a further 24 VCs that have review proofs.) * If the proof function definitions are added and Victor used to submit the VCs to alt-ergo, then there are just 10 VCs (out of 101) left unproven in 8 operations (out of 43). Completion of these remaining VCs requires 17 user rules (all of which are quite simple). It is the combination of proof function definitions and Victor that is effective: Adding the proof function definitions leaves 58 VCs in 30 operations. Using Victor leaves 76 VCs in 36 operations. I hope that this experiment will make the enhancement more likely - supported customers are encouraged to use their influence to promote this change. Although I will not make this extended version of SPARKRules (called SPARKRulesPF) generally available (since it is not a properly tested program) I am prepared to make it available on request provided that the reason for the request is given and an undertaking made to share any results. Replies to this message will reach me, or you can use a sparksure.com address. The program compiles and runs on both Windows 7 and openSUSE 11.3 using the latest versions of Gnat and SPARK (but Victor is available only on Linux at present). Cheers, Phil Thornley