From: Simon Wright <simon@pushface.org>
Subject: Re: What is SPARK about?
Date: Sat, 12 Jun 2010 00:01:51 +0100
Date: 2010-06-12T00:01:51+01:00 [thread overview]
Message-ID: <m2ocfhxjfk.fsf@pushface.org> (raw)
In-Reply-To: d41d71f3-907b-4948-b2b8-784a12439d4c@g39g2000pri.googlegroups.com
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.
next prev parent reply other threads:[~2010-06-11 23:01 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-06-11 20:32 What is SPARK about? Claude
2010-06-11 23:01 ` Simon Wright [this message]
2010-06-11 23:17 ` Yannick Duchêne (Hibou57)
2010-06-12 12:16 ` Peter C. Chapin
2010-06-12 8:30 ` Phil Thornley
2010-06-12 18:09 ` Claude
2010-06-12 19:27 ` Yannick Duchêne (Hibou57)
2010-06-17 5:38 ` Claude
2010-06-13 5:37 ` J-P. Rosen
2010-06-13 8:11 ` Simon Wright
2010-06-13 13:20 ` Robert A Duff
2010-06-17 2:10 ` Claude
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox