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

Tucker Taft taft at adacore.com
Thu Mar 14 15:56:02 CET 2013


On 3/14/13 10:43 AM, Yannick Moy wrote:

>> As far as controlling where the tool would *attempt* to do any proof
>> at all, I thought that would be at a higher level, perhaps more in
>> a configuration file than in the source code.
>
> I don't understand how we can mix SPARK and non-SPARK code then, in the same unit?

What I mean is that if at least part of a subprogram is worth
attempting to prove, then it would be listed in the configuration
file (perhaps using some kind of "wildcarding" pattern).
If a subprogram is not listed in the configuration file,
then it would be skipped in its entirety as far as proof.

Note that whether or not you want something proved is somewhat
different from whether you restrict yourself to SPARK-compatible
constructs within it.  You might enforce the restrictions,
but realize that proof is hopeless at a given state of
development, and want to just rely on run-time checks.

-Tuck



More information about the Spark2014-discuss mailing list