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,48e1a3c594fb62e8,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 Path: g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: SPARK Date: Thu, 13 May 2010 00:55:02 +0200 Organization: Ada At Home Message-ID: NNTP-Posting-Host: FD8vExnEy5iRSNWAUP6U/Q.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:11572 Date: 2010-05-13T00:55:02+02:00 List-Id: Hello, Short title, =E2=80=9CSPARK=E2=80=9D, as short as a subset (joking) I wanted to start some SPARK related questions, ... =E2=80=9CGNAT packag= es in = Linux=E2=80=9D kept apart. Well, sorry for that, my first question gonna be about license. The GPL = = applies to SPARK-GPL (oh? really?). How does it apply ? I'm dubious abou= t = it in this context, because using SPARK to check an implementation does = = not implies any kind of linking to any binary or library, and I did not = = see anywhere something stating there was license restrictions on the usa= ge = of SPARK annotations in Ada sources. What are the concrete restrictions so ? Hope this first question will get a short answer, so let us jump to the = = second question, which is intended to start with one major deal of SPARK= = for people who know/use Ada : Ada subset and restrictions (not to discla= im = or disagree with, mostly to talk and understand more). The Praxis reference for SPARK-95 says : [Praxis SPARK95 3] > SPADE-Pascal was developed essentially by excising from > ISO-Pascal those features which were considered particularly > =E2=80=9Cdangerous=E2=80=9D, or which could give rise to intractable v= alidation > problems - such as variant records, That said, variant record can be emulated by user or program too, as = that's just what were doing many people when there was no language suppo= rt = for that. What is different when the Pascal or Ada variant record compar= ed = to a user or program doing explicitly the same ? May be the answer is ju= st = in one of the last three words : =E2=80=9Cexplicitly=E2=80=9D ? Does this quotation from the Praxis's reference about SPARK suggests SPA= RK = has some troubles with the implicit or the underlying ? If SPARK could know about a formalization of what's going on with varian= t = records, as explicit as would be the same made by the user or program, = would that solve the trick ? What would possibly make this difficult or non-trustable ?