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

Cyrille Comar comar at adacore.com
Thu Mar 14 18:16:07 CET 2013


Le 14/03/2013 17:59, Tucker Taft a écrit :

> 
> My sense is that trying to solve this with a "SPARK" aspect
> now will interfere with the longer term more flexible solution,


I agree that we should rather avoid to be *obliged* to mark explicitly
the code that is in the SPARK subset. That would make the tools very
ineffective for legacy applications.

Having the capability to specify which code is supposed to remain in the
SPARK subset is a good feature. We want to be able to maintain the SPARK
status of some given code and get an error when we start using
unexpected features in it as opposed to lose analysis capability without
noticing it.


> 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,

"SPARK" is the only thing that makes sense to me. We don't want to
express "prove this code", we want to express "keep this code in the
analyzable subset" and isn't it exactly what "SPARK" conveys?


More information about the Spark2014-discuss mailing list