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,UTF8 Path: g2news2.google.com!news3.google.com!feeder.news-service.com!newsfeed.straub-nv.de!news.mixmin.net!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: SPARK Date: Mon, 17 May 2010 03:24:42 +0200 Organization: Ada At Home Message-ID: References: NNTP-Posting-Host: 6sUBlpWRomDanJhrZTDH7A.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org X-Notice: Filtered by postfilter v. 0.8.2 User-Agent: Opera Mail/10.53 (Win32) Xref: g2news2.google.com comp.lang.ada:11671 Date: 2010-05-17T03:24:42+02:00 List-Id: Le Sun, 16 May 2010 20:17:49 +0200, Phil Thornley = a =C3=A9crit: > [...] > 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 - [...] Otherwise this would not be a cut-point any more, indeed, and starting = with a new state, is not a side effect, it's the purpose. > 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.) Unfortunately, I wanted to prove every things (cheese) TBH, I did not work on all, just some and just had a quick overview on = others. > There are (at least) three ways to deal with these (other than > changing the code itself). Sorry for that Er Professor, I've modified it a bit (re-cheese). > 1) Give the Simplifier 'hints' by adding check annotations. > 2) Use the Proof Checker to prove the VCs left after simplfication. As said in another message, this was exactly the purpose : I wanted to = prove without relying on the Checker, in order to have all proofs in the= = text. It seems to be possible, as long as one is explicit enough. > 3) Give the Simplifier more rules to use ('user rules'). I would better like add a very few rule in the whole system, better than= = adding some rules here and there, all being package specific. > My experience is that trying 1) can get very frustrating as the > Simplifier sometimes seems to be extremely stupid. That's an important matter. On an other thread, on the french c.l.a (whe= re = I=E2=80=99ve talked about the same), I was afraid some people may think = SPARK is = not working properly and is unusable for that reason. That's why I = insisted a lot on the Check clause and to not be afraid to detail proofs= = as much as needed. > 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.) I would prefer the choice #3, which seems more logical to me. Just that = = this may be better to add these rules system wide better than on a packa= ge = basis. If I'm not wrong, there is provision for that also. The requirement for a rule to be sound, is indeed important. There may b= e = some rule of thumb in that area, like check all special cases, all speci= al = ranges. As an example, before adding a rule on real, one may carefully = check the rule is valid for multiple combinations of special values and = = bounds and range on each items appearing in the rule, like 0, 1, -1, 0 .= . = 1, 0 .. -1, > 1, < -1, and so on. The same with set, there are special = values as well : empty set/sequence, one element set/sequence, more than= = one, a set included in an other, etc. In that area, I was wondering how built-in rules were choose : from a = well know set of scientist ? Empirically ? By expansion during SPARK's = life ? Others ? I was wondering about it, because I could not find one rule which seems = = important to me, and which does not seems to be part of the predefined s= et = (well, there are actually +500 rules, however, may be some useful rules = = are still missing). > (If you are working through the tutorials in sequence then user rules > are in section 11 - the next to the last). Yes, I've seen it, and I've also read Part 6, which is about the = difference between Check and Assert (I've it later after the question yo= u = were answering). Have a nice day (Peter as well, obviously) Yannick D. -- = There is even better than a pragma Assert: a SPARK --# check. Wanted: if you know about some though in the area of comparisons between= = SPARK and VDM, please, let me know. Will enjoy to talk with you about it= .