[Spark2014-discuss] [M122-037] specifying SPARK sources for analysis

Tucker Taft taft at adacore.com
Thu Mar 14 17:59:23 CET 2013

On 3/14/13 12:08 PM, Yannick Moy wrote:
> On 03/14/2013 05:00 PM, Tucker Taft wrote:
>>> I don't really understand why the simple SPARK / non SPARK distinction
>>> is not relevant. I
>>> see there are issues with tool configuration and code profiles, but to
>>> me they only add to
>>> the SPARK / non SPARK distinction.
>> Mixing these two together is what has created the problem in
>> my mind.
> So if we clearly separate those, and we say we are mostly interested for now in the SPARK
> / non SPARK distinction, is it clear for you then?

My sense is that trying to solve this with a "SPARK" aspect
now will interfere with the longer term more flexible solution,
and generally confuse the issue.  If we want a short-term
solution to this, then I would suggest proposing an aspect
that is not "SPARK."  I have suggested "Proof" and "Analyze."
We could call it "Blah," but calling it "SPARK" leads
to confusion in my mind, as it is mainly being used to control
which parts of the code are analyzed and which parts are presumed
to use run-time checks.

> ... The fact that we can exploit this
> distinction to have a better usability of our tools is indeed a separate issue (although
> that's the one I'm most interested in).

It is not useful if a short-term solution interferes
with a longer-term solution.  If we can get agreement
on a long term solution now, if only at a design level,
then we can base our short-term solution on that.
But if we can't get agreement, or we don't want to
spend the time to get it now, then I would suggest
a short-term solution that is clearly short-term, and
doesn't have a danger of interfering with the ultimate
long-term solution.


More information about the Spark2014-discuss mailing list