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-Thread: 103376,b03962e55f213a92
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nntp.club.cc.cmu.edu!feeder.erje.net!news2.arglkargh.de!news.mixmin.net!eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: What is SPARK about?
Date: Sat, 12 Jun 2010 00:01:51 +0100
Organization: A noiseless patient Spider
Message-ID: <m2ocfhxjfk.fsf@pushface.org>
References: 
 <d41d71f3-907b-4948-b2b8-784a12439d4c@g39g2000pri.googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Injection-Date: Fri, 11 Jun 2010 23:01:52 +0000 (UTC)
Injection-Info: mx03.eternal-september.org;
 posting-host="KCXegvZb5vh43D+f3BR6Ew";
	logging-data="22633"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18xdI54OpmCJpkeSdcdXZFLur2ouN3FQ6s="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (darwin)
Cancel-Lock: sha1:eXCdOeNE+zPcNDWrrSYtSPX18PM=
	sha1:PCnmyINwweAxFw0hTrpvoH/5HT4=
Xref: g2news2.google.com comp.lang.ada:12625
Date: 2010-06-12T00:01:51+01:00
List-Id: <comp.lang.ada>

Claude <claude.defour@orange.fr> writes:

> I means since SPARK is restricted to the best of Ada

The SPARK toolset supports a subset of Ada that it can reason about. As
the SPARK toolset has become more capable (ie, "we" have discovered ways
of programming the machine to reason about more of Ada), so the
supported subset has got larger to match.

As an example, I'm pretty sure SPARK doesn't handle generics; so that
rules out the Container library.