From: Simon Wright <simon@pushface.org>
Subject: Re: Ada features supported by SPARK 2014
Date: Tue, 06 Dec 2016 09:17:57 +0000
Date: 2016-12-06T09:17:57+00:00 [thread overview]
Message-ID: <lyshq1ct6i.fsf@pushface.org> (raw)
In-Reply-To: 0bba1203-42cf-4689-afd1-c417c681f5f6@googlegroups.com
Daniel King <daniel.dmk@googlemail.com> writes:
> In addition, for tasking features, SPARK is limited to the "Ravenscar
> profile", which is basically a set of restrictions on Ada's tasking
> features, to permit static analysis for formal verification.
I found that - as soon as there's anything involving time - I couldn't
work out how to specify flow (when I "fixed" one problem, another would
pop up somewhere else; if I "fixed" that, the first would pop up
again). So I left it up to the tool to infer flow for itself according
to whatever arcane rules it wanted to (not really a satisfactory state
of affairs for something that's supposed to increase my confidence in
the code).
next prev parent reply other threads:[~2016-12-06 9:17 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
2016-12-05 22:01 ` Daniel King
2016-12-06 9:17 ` Simon Wright [this message]
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