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,ASCII Path: g2news1.google.com!news4.google.com!feeder.news-service.com!feeder.visyn.net!visyn.net!aioe.org!not-for-mail From: =?iso-8859-15?Q?Yannick_Duch=EAne_=28Hibou57=29?= Newsgroups: comp.lang.ada Subject: Re: SPARK understand me very well... me neither Date: Sat, 14 Aug 2010 18:44:11 +0200 Organization: Ada At Home Message-ID: References: <2308d0a0-8fdb-41a0-b2dc-6b30a2bf2f18@v41g2000yqv.googlegroups.com> NNTP-Posting-Host: YYagVKn1YrNkilfPXbyxag.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.60 (Win32) Xref: g2news1.google.com comp.lang.ada:13290 Date: 2010-08-14T18:44:11+02:00 List-Id: Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley = a =E9crit: > Yannick, I realise that you are an enthusiast for this but it's not > the way that the job is done in practice - it doesn't scale up for > real problems. When it takes seven proof statements to (fail to) > prove a simple multiplication then this method isn't practicable for > the sorts of expressions that appear in the real-world models of > embedded systems. That is precisely the matter I was wondering about. It appears all my = attempt always end to be too much complicated. > So we shouldn't be publicising this approach in sites such as Rossetta= > Code. OK. > For this particular example, I don't understand why you haven't used > the obvious precondition: > --# pre A * B in Integer; Because I did not knew this was feasible. May be due to a background: I = = use to write less or more formal comment in Pascal or Ada source, to sho= w = that this and that was valid or how this could be valid. So all my attem= pt = so far was focusing on the How Be Valid (and though SPARK was working th= is = way also). If i understand you, there is a more declarative approach. Is= = that it ? > The version of the precondition that will work best (measured by > leaving the lowest number of unproven VCs) depends on how the calling > code ensures that it meets the precondition. This is one of the reason I am thinking about the How Be Valid. Balancin= g = your way and the (not so good) way I used so far, I would say one says = How, the other does not. > The easiest way to achieve this (for general purpose functions like > Multiply) is by having the subtypes of the parameters as constrained > as possible, so, as long as the bounds on the two terms are small > enough, meeting this simpler version of the precondition is > automatic. Yes. That is exactly what I had in a Pascal application I remember of. I= = had a kind of screen area, and I had to be sure the area could always be= = computed without overflow. I defined a type for area, and a type for = height and width, so that the maximum of width and height could never = commit an overflow and area could always be computed in any case. This f= at = more simple to check for that checking less constrained width and height= = would not commit an overflow. The reason why I did not used it here, is because I did not see a = legitimate way to restrict the input type beside of the result type. > OTOH, if the bounds of the parameter subtypes can't ensure the > precondition, then the program has to use a defensive check, in which > case your version of the precondition may work better (if the > defensive check is exactly that precondition). That is the case where input cannot be constrained, which is, if this ha= s = to be fully general and generic. While the way I exposed with the Pascal= = example above, is better whenever possible. > In a well-designed program, the subtype constraints should match the > usage of the variables of the subtypes Agree, except that I could not see a way to restrict here. > So I would much prefer the simple and obvious version of the > precondition and code to be the version on Rosetta Code so that anyone= > browsing that site for information about SPARK doesn't get a wrong > view of the language. That is the target and the reason why I posted the question here. Hopful= ly = I get the good anwser. Wish I had read such a reply priorly, this would have save me lot of = headache. Will try to revisit all my approach with this ideas in mind. Hope you are not too much tired with my beginner's 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.