[Spark2014-discuss] [M122-037] specifying SPARK sources for analysis
taft at adacore.com
Thu Mar 14 16:02:01 CET 2013
On 3/14/13 10:45 AM, Arnaud Charlet 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. The pragmas in the
>> source code were more about controlling what features the programmer
>> is allowed to use, much like pragma Restrictions, but with a more
>> flexible local override capability.
> Here I suspect there's a discrepency of intent between people, because some
> people do want to be able to specify when to do proof or not, and that's
> what we mean by in/out SPARK, so that's a major discrepency and this
> explains why we seem to be in disagreement while we probably aren't actually.
> In other words, different people seem to be widely different views on what
> we are trying to achieve here, and there's as a result a discrepency in terms
> of scope and usability.
I agree, there are two somewhat different issues here, one is
where you want the "prover" to try to do its work, and the other
is what features you want to restrict. I believe the first might
best be handled with a configuration file, as it may vary over time
and depending on the project. The second, namely the restrictions
to be imposed, is fundamental to what language constructs may be
written at a given place, and should be visible in the source code.
It sounds like we may need two different mechanisms, though
clearly there is some relation between the two.
>> This feels like a topic deserving of a "SPARK Issue" as we don't
>> seem to be converging just through e-mail back and forth.
> I don't see how a "SPARK Issue" will solve anything. Instead we need to
> resolve this during a concall IMO. ...
The point of a "SPARK Issue" is for someone to capture all of
the alternatives, with rationale and trade-offs well documented,
and with examples. E-mail is a rather poor substitute for that
kind of reasoned argument. Trying to resolve these kinds of
things in a conference call, without first having someone lay
out the various alternatives in a clear fashion, is a mistake in
More information about the Spark2014-discuss