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:
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 Off.
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 SPARK_Mode Off. Note that this may require repeating a pragma SPARK_Mode (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 SPARK_Mode (Off), then that pragma will need to be repeated in the package body.