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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,48e1a3c594fb62e8 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,CP1252 Path: g2news2.google.com!postnews.google.com!c13g2000vbr.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK Date: Sun, 16 May 2010 11:17:49 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1274033869 23211 127.0.0.1 (16 May 2010 18:17:49 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 16 May 2010 18:17:49 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: c13g2000vbr.googlegroups.com; posting-host=80.177.171.182; 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),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:11662 Date: 2010-05-16T11:17:49-07:00 List-Id: On 15 May, 21:23, Yannick Duch=EAne (Hibou57) wrote: [big snip :-] > What does =93cut point=94 means precisely ? Is it related or similar to t= he =A0 > unfortunately too much famous Prolog's cut ? This seems to be the next = =A0 > question to be answered, and a focus to care about for peoples learning = =A0 > SPARK. There may be multiple paths to any point (before/after/between executeable statements). For the purposes of VC generation, a "cut point" is a point in the code that terminates all the paths that reach it and there is a single path starting at that point. The hypotheses of VCs include the local state that has been defined along a path, and each path to a point will have different versions of these hypotheses. Therefore the hypotheses that are generated in VCs that follow a cut point cannot include any of the hypotheses that have been included in the VCs before the cut point - unless they are included in the assertion at the cut point and therefore proved to be true for every path that reaches that cut point. > About one of the most worthy thing with proving : what's the better way t= o =A0 > give hints to the prover ? Is it =93assert=94 or =93check=94 ? This examp= le =A0 > suggest the best way is =93check=94. Is this example representative of mo= st =A0 > cases or a just a special case ? You should always use 'check' when giving the Simplifier a hint - then you don't lose any of the local state information. Another key point to understand is that the Simplifier does not prove all provable VCs (so when the tutorials ask you to "make all VCs provable" don't expect to get all the VCs proved by the Simplifier.) There are (at least) three ways to deal with these (other than changing the code itself). 1) Give the Simplifier 'hints' by adding check annotations. 2) Use the Proof Checker to prove the VCs left after simplfication. 3) Give the Simplifier more rules to use ('user rules'). My experience is that trying 1) can get very frustrating as the Simplifier sometimes seems to be extremely stupid. 2) works OK but isn't practical for any software under development as the proof scripts that are created (and are needed each time the VCs are generated) are extremely fragile to minor changes in the software. The current recommendation is to use 3) - create user rules as appropriate. These are easy to write and usually work as expected. (But they are a very powerful mechanism, so are correspondingly dangerous - it is quite easy to create unsound user rules.) (If you are working through the tutorials in sequence then user rules are in section 11 - the next to the last). Cheers, Phil