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

Yannick Moy 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 
same unit?
-- 
Yannick Moy, Senior Software Engineer, AdaCore


More information about the Spark2014-discuss mailing list