[Spark2014-discuss] [M122-037] specifying SPARK sources for analysis
moy at adacore.com
Thu Mar 14 15:43:08 CET 2013
On 03/14/2013 03:30 PM, Tucker Taft wrote:
> For example, you want to have a call on a logging function,
> but you don't want to have to analyze the "correctness" of
> the call. Or you want to have an exception handler but you
> don't want the presence of the exception handler to prevent
> the rest of the subprogram from being analyzed.
Both are examples of "hiding" where you want to ignore something the
program does. I think this is incompatible with the direction we try to
give to SPARK 2014, where we want to provide better guarantees to the user.
It is true that "hiding" is possible in SPARK 2005. But giving axioms is
also possible in SPARK 2005, and we have rejected this possibility in
SPARK 2014, in order precisely to provide better guarantees.
> Apparently the current users of SPARK make use of the "hide" capability.
> It seems feasible to "skip over" some statements during the analysis
> of a subprogram, which isn't quite the same as doing a proof on "parts"
> of a subprogram.
If we provide a hiding mechanism, the burden is on the user to define
what assumptions are required on the hidden code for which guarantees.
Same as with axioms. This is what we want to avoid. We have seen
repeated cases where such mechanisms just destroy all guarantees (see
the experiences of David Lesens with SPARK at Astrium, and the recent
non-obvious wrong axioms that Paul Jackson found in his axioms)
> 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
Yannick Moy, Senior Software Engineer, AdaCore
More information about the Spark2014-discuss