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 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. It includes in particular:
rich types (subtypes with bounds not known statically, discriminant records, subtype predicates, access types)
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] or [Ada 202X]) is used to denote that a feature defined in Ada 2005 (resp. Ada 2012 or Ada 202X) is supported in SPARK, and the marker [Ravenscar/Jorvik] is used to denote that a concurrency feature from Ada which belongs to the Ravenscar or Jorvik profiles 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 GNAT Studio or
GNATBench) via the menu item.
- 5.1. Language Restrictions
- 5.2. Subprogram Contracts
- 5.3. Package Contracts
- 5.4. Type Contracts
- 5.5. Specification Features
- 5.5.1. Aspect
Constant_After_Elaboration
- 5.5.2. Aspect
No_Caching
- 5.5.3. Aspect
Relaxed_Initialization
and Ghost AttributeInitialized
- 5.5.4. Aspect
Side_Effects
- 5.5.5. Attribute
Loop_Entry
- 5.5.6. Attribute
Old
- 5.5.7. Attribute
Result
- 5.5.8. Aggregates
- 5.5.9. Conditional Expressions
- 5.5.10. Declare Expressions
- 5.5.11. Expression Functions
- 5.5.12. Ghost Code
- 5.5.13. Quantified Expressions
- 5.5.1. Aspect
- 5.6. Assertion Pragmas
- 5.7. Overflow Modes
- 5.8. Object Oriented Programming and Liskov Substitution Principle
- 5.9. Pointer Support and Dynamic Memory Management
- 5.10. Concurrency and Ravenscar Profile
- 5.11. SPARK Libraries
- 5.11.1. SPARK Library
- 5.11.2. Big Numbers Library
- 5.11.3. Functional Containers Library
- 5.11.4. Formal Containers Library
- 5.11.5. Containers and Executablity
- 5.11.6. SPARK Lemma Library
- 5.11.7. Higher Order Function Library
- 5.11.8. Input-Output Libraries
- 5.11.9. Strings Libraries
- 5.11.10. C Strings Interface
- 5.11.11. Addresses to Access Conversions
- 5.11.12. Cut Operations