pragma SPARK_Mode [(On | Off)] ;
In general a program can have some parts that are in SPARK 2014 (and follow all the rules in the SPARK Reference Manual), and some parts that are full Ada 2012.
The SPARK_Mode pragma is used to identify which parts are in SPARK 2014 (by default programs are in full Ada). The SPARK_Mode pragma can be used in the following places:
privatekeyword of a library-level package spec
beginkeyword of a library-level package body
Normally a subprogram or package spec/body inherits the current mode that is active at the point it is declared. But this can be overridden by pragma within the spec or body as above.
The basic consistency rule is that you can’t turn SPARK_Mode back
On, once you have explicitly (with a pragma) turned if
Off. So the following rules apply:
If a subprogram spec has SPARK_Mode
Off, then the body must
also have SPARK_Mode
For a package, we have four parts:
For a package, the rule is that if you explicitly turn SPARK_Mode
Off for any part, then all the following parts must have
Off. Note that this may require repeating a pragma
Off) in the body. For example, if we have a
configuration pragma SPARK_Mode (
On) that turns the mode on by
default everywhere, and one particular package spec has pragma
Off), then that pragma will need to be repeated in
the package body.