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

Tucker Taft taft at adacore.com
Thu Mar 14 16:08:00 CET 2013


On 3/14/13 11:01 AM, Yannick Moy wrote:

> ok I see your distinction now. At first, we plan to simply attempt proof on everything in
> SPARK, hence the need to be able to identify which code is in SPARK according to the user.
> What I meant is that this information needs to be in the code, and I think we agree.

But I think trying to make these one mechanism is what is creating the
problem.  I think they may be fundamentally different issues, and
saying something is either "in SPARK" or "not in SPARK" is apparently
too "binary" for some people.  They would rather indicate what sort
of a set of restrictions they want to impose (currently dubbed a "code
profile"), which might take them below the "SPARK 2014" line.
One of the problems is that exactly what is the SPARK 2014
line may vary from release to release of the tool.
It will not be good if the meaning of these pragmas changes
over time.  I think we want pragmas connected to specific Ada features.
At any given time, the tool may have trouble proving code that uses
certain features, but later it may be able to handle it.  You don't
want to have to re-annotate your code just because the tool has
gotten smarter.

> We can always add more control on the tool side, if needed, possibly with patterns as you
> suggest. These may not be in the code, and in any case they are not part of SPARK 2014.

I don't think we can delay this, at least from a design point of
view, because the control of the tool and the control of which
Ada features are permitted in a given piece of source text, are
not really the same thing, and trying to merge them into one
specification seems to be creating a problem.

-Tuck



More information about the Spark2014-discuss mailing list