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 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,1d52a75fd633fefc X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-02-24 08:21:34 PST Path: supernews.google.com!sn-xit-02!supernews.com!isdnet!newsfeeds.belnet.be!news.belnet.be!btnet-peer1!btnet-feed5!btnet!mendelevium.btinternet.com!not-for-mail From: Nick Williams Newsgroups: comp.lang.ada Subject: Re: Ada to C++ translator? Date: Sat, 24 Feb 2001 16:22:37 +0000 Organization: BT Internet Message-ID: <3A97DFCD.3010503@acm.org> References: <3A844255.24A4DBA3@lmco.com> <3A866B28.CE67B4A0@yyy.zzz> <3A8C6AA3.3F90043D@lmco.com> <%Wvk6.102$aw5.380@www.newsranger.com> <9713k0$6ao$1@nh.pace.co.uk> <976jbu$3p4$1@nh.pace.co.uk> NNTP-Posting-Host: host213-1-173-243.btinternet.com Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit User-Agent: Mozilla/5.0 (X11; U; Linux 2.4.0 i686; en-US; 0.8) Gecko/20010215 X-Accept-Language: en Xref: supernews.google.com comp.lang.ada:5511 Date: 2001-02-24T16:22:37+00:00 List-Id: Marin David Condic wrote: >> There's a difference between a compiler which doesn't support the full >> language and a project choosing not to use the full language! > And your point would be? :-) Seriously, I understand there is a distinction, > but I don't know that it makes any difference. SPARK is a chosen subset of > Ada and I'd presume that if one bought the SPARK compiler that it would > compile only the SPARK subset. (Or at least someone might choose to > implement a compiler for SPARK that way.) You'd have difficulty buying the SPARK compiler; as there isn't one :-) >From the Ada perspective, SPARK is indeed a subset; since whatever is a valid SPARK program is also a valid Ada program, but the converse does not hold. However, just because an Ada program uses the subset of the Ada language which is valid in SPARK will (most likely) not make that program valid in SPARK: the SPARK language has a considerable variety of non-compilable statements (which look to an Ada compiler like comments) which are not optional when constructing SPARK programs. It also has restrictions on the use of language features which can make it harder to prove properties of your program. > (SPARK doesn't call itself "Ada" and isn't validated, right?) Well, the 'A' in SPARK does stand for Ada ... and the only validation is a relatively detailed and complete formal semantics of the language :-) Cheers, Nick.