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: 103376,af40877501f46910 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Path: g2news1.google.com!news4.google.com!feeder.news-service.com!weretis.net!feeder4.news.weretis.net!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 understand me very well... me neither Date: Sun, 15 Aug 2010 00:20:19 +0200 Organization: Ada At Home Message-ID: References: <2308d0a0-8fdb-41a0-b2dc-6b30a2bf2f18@v41g2000yqv.googlegroups.com> NNTP-Posting-Host: vW41ugf3bPGxhjQJ6q2hXA.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.61 (Win32) Xref: g2news1.google.com comp.lang.ada:13309 Date: 2010-08-15T00:20:19+02:00 List-Id: Le Sat, 14 Aug 2010 23:50:08 +0200, Jeffrey Carter = a =C3=A9crit: > It doesn't prove anything, and it's not supposed to. It's a = > precondition. It says, "This precondition must be true for this = > operation to give correct results." It is the caller's duty to meet th= e = > precondition. I understand that objection ; but in the mean time, isn't it the purpose= = of an interface to ease use and to help to manage things ? The = precondition is part of the interface as much as the function signature = is = after all. I will need some time to try an imagine new approachs. The one I was using until now was more looking mathematical proof (by th= e = way, the same kind of you may have with VDM or something of the like), = that is a step by step hypothesis -> conclusion -> new hypothesis -> new= = conclusion, each possibly referring to previous conclusions. That is the= = reason why I oftenly number each step and refer to these in conclusions = as = =E2=80=9C... -- from (x) and (y)=E2=80=9D where x and y are numbers of p= revious steps. = Indeed, this approach does not seems to be well suited with SPARK and en= ds = into unsolvable things. The fact it does not only validate proof, but al= so = tries to prove things it-self is an important fact with consequences. Th= is = is not really a validator, this is half validator and half automatic = prover. And this impacts the way it works. You cannot expect it to follo= w = your step-by-step proof (because it may use this or that hypothesis its = = own way, possibly going into long backtrackings or explorations), and yo= u = cannot expect it to prove every things automatically (that point is = obvious). This makes it unfamiliar to me, so I will have to figure some = = other ways to do with it. Will have some opportunities, as I would like to test it on some other = Rosetta examples (along with some personal uses I am planning and alread= y = started to test).