5. Overview of SPARK Language

This chapter provides an overview of the SPARK language, detailing for each feature its consequences in terms of execution and formal verification. This is not a reference manual for the SPARK language, which can be found in:

  • the Ada Reference Manual (for Ada features), and
  • the SPARK 2014 Reference Manual (for SPARK-specific features)

More details on how GNAT compiles SPARK code can be found in the GNAT Reference Manual.

SPARK can be seen as a large subset of Ada with additional aspects/pragmas/attributes, the latest version SPARK 2014 being a much larger subset than previous versions of SPARK. It includes in particular:

  • richer types (subtypes with bounds not known statically, discriminant records, type predicates)
  • more flexible features to structure programs (function and operator overloading, early returns and exits, raise statements)
  • code sharing features (generics, expression functions)
  • object oriented features (tagged types, dispatching)
  • concurrency features (tasks, protected objects)

In the rest of this chapter, the marker [Ada 2005] (resp. [Ada 2012]) is used to denote that a feature defined in Ada 2005 (resp. Ada 2012) is supported in SPARK, and the marker [Ravenscar] is used to denote that a concurrency feature from Ada which belongs to the Ravenscar profile is supported in SPARK. The marker [SPARK] is used to denote that a feature is specific to SPARK. Both the GNAT compiler and GNATprove analyzer support all features listed here.

Some code snippets presented in this section are available in the example called gnatprove_by_example distributed with the SPARK toolset. It can be found in the share/examples/spark directory below the directory where the toolset is installed, and can be accessed from the IDE (either GPS or GNATBench) via the Help ‣ SPARK ‣ Examples menu item.