From: Daniel King <daniel.dmk@googlemail.com>
Subject: Re: Ada features supported by SPARK 2014
Date: Mon, 5 Dec 2016 14:19:31 -0800 (PST)
Date: 2016-12-05T14:19:31-08:00 [thread overview]
Message-ID: <d4a8672d-bfad-4ca9-b821-033e9e45cc94@googlegroups.com> (raw)
In-Reply-To: <o24n9c$auu$1@dont-email.me>
On Monday, 5 December 2016 17:48:45 UTC-4, G.B. wrote:
>
> There was/is no/limited support for generic units.
To clarify, SPARK language versions 83, 95, and 2005 had no support for generic units at all (as far as I know), but the latest version of SPARK has full support for generic units (as long as they don't use any Ada language features 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 parameters 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 library: https://github.com/damaki/libkeccak
next prev parent reply other threads:[~2016-12-05 22:19 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-12-05 20:36 Ada features supported by SPARK 2014 pault.eg
2016-12-05 21:10 ` Shark8
2016-12-07 18:09 ` Jacob Sparre Andersen
2016-12-05 21:48 ` G.B.
2016-12-05 22:19 ` Daniel King [this message]
2016-12-05 22:01 ` Daniel King
2016-12-06 9:17 ` Simon Wright
2016-12-06 13:26 ` Daniel King
2016-12-09 8:24 ` Robert Eachus
2016-12-09 17:21 ` Adam Jensen
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox