[Spark2014-discuss] [M122-037] mark code in or out SPARK

Arnaud Charlet charlet at adacore.com
Wed Mar 27 17:15:47 CET 2013

> FWIW, I can understand why people don't like "SPARK_mode", but until
> now I find it is the best proposal ...

Indeed, that's the general feeling (so far the best name, but if someone
comes up quickly with a better one, let's consider it).

We've discussed during a concall yesterday (Steve, Stuart, Tuck, John, Arno)
about the proposal and after a few small changes agreed that the proposal
looks good.

Cyrille: in particular we went back to my initial proposal to mark spec+body
at the same time, this made more sense to all the people in the concall,
and in particular that's the standard semantic for all/most Ada 2012
aspects (if an aspect is on a spec, it applies to the whole entity, spec+body).

Steve/Trevor mentioned that one delicate area is when marking out of SPARK
(SPARK_Mode (Off)) a private part: how to ensure consistency between the
public part of private types and its private part, and what kind of assumptions
the tools should make on private types since we cannot put annotations on
private types.
For now, we've decided to solve this issue by documenting the
assumptions/constraints (e.g. assume the object isn't initialized for
soundness?), and in a later revision of the language, we might consider
addition new annotations so that users can specify whether/how private types
are initialized.

In any case, we agreed that documentation would be good enough for now,
since SPARK 2005 does not address this issue either (private part "hidden").

See latest/updated proposal here:


Steve, may I reassign this ticket to you so that you can work (with Trevor
if needed) on the RM wording, and then we can start ASAP implementation
in the front-end? Would be good to have the front-end part done for the
GPL 2013 releases, even though that's not blocking.


More information about the Spark2014-discuss mailing list