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,494ac732c5488b7f X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 Path: g2news2.google.com!news4.google.com!feeder.news-service.com!tudelft.nl!txtfeed1.tudelft.nl!zen.net.uk!dedekind.zen.co.uk!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: What does it prove? Date: Mon, 31 May 2010 03:17:32 +0200 Organization: Ada At Home Message-ID: References: <4bffc379$0$2374$4d3efbfe@news.sover.net> NNTP-Posting-Host: f1hJjE4MxMa4iAvHeIkx2A.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:12164 Date: 2010-05-31T03:17:32+02:00 List-Id: Le Fri, 28 May 2010 15:25:50 +0200, Peter C. Chapin = a =C3=A9crit: > It is common to talk about SPARK proofs but of course what the = > Simplifier is > actually proving are the verification conditions generated by the = > Examiner. > Formally this leaves open the question of if those verification = > conditions > have anything to do with reality or not. The question, =E2=80=9Cwhat does it prove ?=E2=80=9D, raise another coro= llary question, = which is =E2=80=9Cwhat can it says ?=E2=80=9D or =E2=80=9Cwhat can it ta= lks about ?=E2=80=9D. I'm currently trying to make proofs on some binary stuffs, which has = always seems obvious to me, and at the time of trying to prove it, I see= I = can't even prove the third of the initial postcondition I wanted my = functions to have, because there are some I can't prove at all (I'm not = = talking about RTC, rather about postcondition expressing properties, and= = it is far less easy than proving RTC conditions). If is funny to note that these difficulty are a consequence of SPARK tie= d = to Ada. An example : Ada has modular type, but can't see modular types h= as = polynomials, and the relevant modal, which could help, would be this one= : = polynomial. Has Ada don't has this, SPARK doesn't too. Another things also : sometime, it is better to make proof on an abstrac= t = algorithm, which not efficient, and it is too much difficult to the same= = proof (prove postconditions from preconditions and the algorithm) with t= he = efficient version. However, it would be more easy to demonstrate than th= e = efficient algorithm is an equivalent transformation of the more abstract= = non-efficient one. I mean, prove something on function F, demonstrate function G is = equivalent to function F, so as legally assert the postconditions of F a= re = also prove on G, because there was on F and G is equivalent to F. This is another kind of thing SPARK cannot express or talk/say about. This may be the start of some answers to the question =E2=80=9Cwhat can = it proves = ?=E2=80=9D or =E2=80=9Cwhat can't it proves ?=E2=80=9D, which are simila= r questions. -- = There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.