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,ec6f74e58e86b38b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!not-for-mail From: =?iso-8859-15?Q?Yannick_Duch=EAne_=28Hibou57=29?= Newsgroups: comp.lang.ada Subject: Re: Lost in translation (with SPARK user rules) Date: Wed, 26 May 2010 22:56:38 +0200 Organization: Ada At Home Message-ID: References: <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com> <4bfd2d05$0$27598$ba4acef3@reader.news.orange.fr> <4bfd7728$0$27592$ba4acef3@reader.news.orange.fr> NNTP-Posting-Host: VsdMw8HJ6uo7b6guDb/gnA.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15; 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:12050 Date: 2010-05-26T22:56:38+02:00 List-Id: Le Wed, 26 May 2010 21:32:02 +0200, Pascal Obry a =E9c= rit: > Right. I think the response to this is pragmatism and cost. For non > critical softwares do you think it is reasonable to use SPARK? This is= > only a matter of trade-off I think. So, depends on how it is balanced. If the component of an application of an application, is to be executed = = thousand of times in a day or in a week, and especially if this is to be= = executed automatically, the trade-off should give weight to verifiabilit= y, = even for applications which are not know to be critical in the usual sen= se. For others, I would say proofs could help to understand why it works (no= t = just how). This could be nice for pedagogy, as a formal comments is alwa= ys = more readable than implicit human language (not that I don't like the = latter, just that it is sometime too much weak). And for maintainability= , = like modifying this and that for more efficiency, or simply adding a = functionality, with the insurance nothing will be broken on the way. What kind of trade-off should not care ? (note: I was thinking about also some other reasons, however not exposed= , = to be short) > [...] where data are read from the same socket but > two consecutive read won't return the same value. There is way in SPAR= K > to deal with that, to avoid SPARK complaining that you have ineffectiv= e > code... not straight forward! > > Pascal. I see what the subject was looking like I was thinking about something. With my attempted pre/post/check in mind= , = I was reading the SPARK source, and noticed one thing : the postconditio= ns = in the SPARK sources, are far less detailed than what I was attempting t= o = do with my packages. To be honest, I was not only to prove there will no= t = be any runtime error, I was also using postconditions to express = properties and logics. So obviously, this ends in much more difficult = complicated things to demonstrate. This may be a rule of thumb with SPARK : first, try to have a program = proved to be runtime error free, then after only, when that done, try to= = add more to express logic properties. May be I was somewhere between proof of absence of runtime error and dat= a = refinement (I mean what in french is named =AB r=E9ification =BB). Possi= bly = SPARK do not the best with the latter. Finally, stating a procedure or = function has this and that logic property, is another way to state this = is = the concrete implementation of the abstraction which has these same = properties ; so this is refinement/reification. Perhaps SPARK can do that... a bit, and perhaps I was wrong to expect it= = could fully do that. So this rule of thumb : start with proof of no runtime error first, and = = only later try more and don't expect this is required to succeed ? However, being able to add rules which could be applied the same way = embedded rules are, would really be nice. While I suspect this would not= = be compatible with some efficiency requirements of the SPARK Simplifier = = (if only I could build the Simplifier from modified source, but I can't)= . -- = There is even better than a pragma Assert: a SPARK --# check.