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=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.157.26.50 with SMTP id a47mr15272181ote.120.1480976372180;
        Mon, 05 Dec 2016 14:19:32 -0800 (PST)
X-Received: by 10.157.15.143 with SMTP id d15mr3808339otd.2.1480976372134;
 Mon, 05 Dec 2016 14:19:32 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!p16no3023600qta.1!news-out.google.com!m27ni1906qtf.1!nntp.google.com!n6no3024531qtd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Mon, 5 Dec 2016 14:19:31 -0800 (PST)
In-Reply-To: <o24n9c$auu$1@dont-email.me>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=156.57.114.26;
 posting-account=qa2LvwoAAADwbTxJVBI5rHWSlh3aClXp
NNTP-Posting-Host: 156.57.114.26
References: <c1a607a7-dce1-47a2-b4e5-7eba44ad4647@googlegroups.com>
 <o24n9c$auu$1@dont-email.me>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <d4a8672d-bfad-4ca9-b821-033e9e45cc94@googlegroups.com>
Subject: Re: Ada features supported by SPARK 2014
From: Daniel King <daniel.dmk@googlemail.com>
Injection-Date: Mon, 05 Dec 2016 22:19:32 +0000
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Xref: news.eternal-september.org comp.lang.ada:32629
Date: 2016-12-05T14:19:31-08:00
List-Id: <comp.lang.ada>

On Monday, 5 December 2016 17:48:45 UTC-4, G.B.  wrote:
>=20
> There was/is no/limited support for generic units.

To clarify, SPARK language versions 83, 95, and 2005 had no support for gen=
eric units at all (as far as I know), but the latest version of SPARK has f=
ull support for generic units (as long as they don't use any Ada language f=
eatures that are not allowed in SPARK).

One consequence of this is that you can't actually run the proof tools on a=
 generic unit directly, since it's not known if it's in SPARK or not until =
the unit is instantiated (for example, what if one of the generic parameter=
s is an access type, which is not allowed in SPARK). So the proof tools are=
 run on each *instantiation* of a generic unit.

I've used generics heavily in one of my SPARK projects - a SHA-3 hashing li=
brary: https://github.com/damaki/libkeccak