[Spark2014-discuss] SPARK 2014 profiles/policies

Arnaud Charlet charlet at adacore.com
Tue Mar 12 18:46:20 CET 2013


> And regarding profiles (now Code Policies), the language design team
> should note above the implied requirement: the best way to achieve this is
> probably to allow users to tune/edit policies so that an adjustment such as
> permitting operator overloading could be made to a more restrictive
> pre-defined policy such as "Classic SPARK".

By the way, I disagree with this, this shouldn't be a requirement.

"Classic SPARK" (better called "SPARK 2005") contains lots of unnecessary
restrictions that very few people will want to inherit from, so it's
actually much better to add a few restrictions similar to what was in
SPARK 2005, rather than start from SPARK 2005 restrictions and remove lots
of unnecessary one. I've just had a look, and among the dozens of checks
done in GNAT to implement pragma SPARK (about 150 different checks), I could
find only 2 or 3 that might be useful for SPARK 2014 users. I'm sure
I missed another 3 or 4, but still, that's about 2% of the SPARK checks that
we are talking about, so having a mechanism where we start from SPARK 2005
and where we then remove 98% of the restrictions does not seem very useful.

In other words, we should have an opt-in mechanism, but no opt-out mechanism.

This will both allow to reuse the existing Ada Restrictions/Profile mechanism
and remove the need for introducing a new, complex ad hoc mechanism.

Arno


More information about the Spark2014-discuss mailing list