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

Tucker Taft taft at adacore.com
Thu Mar 14 16:31:02 CET 2013

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

> ... I have a third control in mind, which is simpler and more essential than the tool control
> or feature control: the SPARK/not SPARK boundary. Tool control can be delayed if we agree
> the tool initially deals with SPARK code only (possibly notifying the user when it cannot
> handle some features yet).

Perhaps if we dropped the terms "SPARK" and "non SPARK" and focused
on whether we want to "attempt proof" or not, then this would clarify
things.  "SPARK" means too many things at this point, and using it
as a way to turn on or off proof seems like it has pushed things to
a breaking point.  How about "Proof => On" or "Proof => Off".  This
would be to some degree orthogonal to the "Code Profile" notion.
I think this might help to defuse the conflict.


More information about the Spark2014-discuss mailing list