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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no 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-7-bit Path: g2news1.google.com!postnews.google.com!w30g2000yqw.googlegroups.com!not-for-mail From: Mark Lorenzen Newsgroups: comp.lang.ada Subject: Re: SPARK code samples Date: Wed, 11 Aug 2010 10:32:43 -0700 (PDT) Organization: http://groups.google.com Message-ID: <1b7d07a3-563c-4c0e-93db-e30a94e32932@w30g2000yqw.googlegroups.com> References: C8888F59.14CCDC%yaldnif.w@blueyonder.co.uk NNTP-Posting-Host: 193.163.1.105 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: posting.google.com 1281547964 26634 127.0.0.1 (11 Aug 2010 17:32:44 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Wed, 11 Aug 2010 17:32:44 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: w30g2000yqw.googlegroups.com; posting-host=193.163.1.105; posting-account=Srm5lQoAAAAEMX9rv2ilEKR6FDPapmSq User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; da; rv:1.9.2.8) Gecko/20100722 Firefox/3.6.8,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:13132 Date: 2010-08-11T10:32:43-07:00 List-Id: On 11 Aug., 18:33, "(see below)" wrote: > On 11/08/2010 17:07, in article > fa1507ef-77a8-4a28-b271-2293c5115...@j8g2000yqd.googlegroups.com, "Mark > > Lorenzen" wrote: > > On 11 Aug., 13:38, Ada novice wrote: > > >> Thanks for this information. I'm interested to learn SPARK. If I > >> understand correctly, SPARK aligns itself well with Ada 95 and not yet > >> with Ada 05. Is this because of the strictness of SPARK to provide > >> highly reliable codes and hence it contains only well-tested features > >> (subset of Ada features)? It would be interesting to see some SPARK > >> codes on the wiki page building over time. > > > Not quite. SPARK is a proper subset of Ada and is amenable to static > > analysis. This has (in principle) nothing to do with if an Ada feature > > is well-tested or not. You should think of SPARK as a language in its > > own right and not as a subset of some other language. > > Why? > > -- > Bill Findlay > chez blueyonder.co.uk I take it you refer to my last sentence. First of all because SPARK is not only a set of restrictions imposed on the Ada language, SPARK also mandates the use of annotations (and even more so if you want to prove program correctnes). As SPARK annotations are written as Ada comments, it is true that every SPARK program is also an Ada program and that may be why people often think of SPARK as "just" a subset of Ada [1]. I also think there is a risk of getting stuck with SPARK if you try to design a SPARK program with Ada in mind. You constantly bump into a useful feature of Ada that is not in SPARK (discriminated types, array slicing etc.) and you think "why the h... isn't that a part of SPARK when it's so easy to do in Ada?". So it's probably a way of tuning your mindset from "Ada with restrictions" into SPARK. [1] Purists may argue that even with the presence formal annotations, every SPARK program will be a member of the set of all Ada programs that include every permutation of every legal comment in every legal place. Or what? - Mark L