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,b36bbdc1595d0665 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!news4.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: SPARK code samples Date: Wed, 11 Aug 2010 18:45:33 +0200 Organization: Ada At Home Message-ID: References: <1iq8kg021bo4v$.s51i2enx3fzo.dlg@40tude.net> NNTP-Posting-Host: wRBcePl7nU3x+PaBbkDMVA.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:13128 Date: 2010-08-11T18:45:33+02:00 List-Id: Le Wed, 11 Aug 2010 18:07:51 +0200, Mark Lorenzen = a =E9crit: > Not quite. SPARK is a proper subset of Ada and is amenable to static > analysis. Yes > This has (in principle) nothing to do with if an Ada feature > is well-tested or not. SPARK is actually an Ada subset ;) And it elvoves toward more support of= = this or that Ada feature... while not all, and it will probably never = support all, this one is true. > You should think of SPARK as a language in its > own right and not as a subset of some other language. From an abstract point of view, yes. There is SPARK and SPADE, and SPAR= K = Examiner is based on SPADE Examiner (if I am not wrong... Rod will corre= ct = if needed). SPADE mainly came from Pascal, which was the first subsetted= . = But SPARK is still based on Ada. There is SPARK no SPARK Modula, no SPAR= K = Oberon and so on. > Although SPARK > constantly evolves it will never evolve into a language with the same > feature-set as Ada - no matter how well tested all Ada festures one > day will be. That precisely matter. If some feature are excluded, this is solely = because they either does not enforce readability (overloading), are not = = predictable enough (while this depend on the state of the art) and could= = be in theory, but not practical or really workable way to do was found (= if = this end up into a SPARK which requires days to validate 10 lines, this = is = not good). Excluded features are excluded for some known reasons, most = being documented in the SPARK Language Reference Manual. By the way, the SPARK Language Reference Manual stick to the one Ada : i= t = use the same section numbering, naming, and so on. -- = 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.