SPARK is a programming language and a set of verification tools designed to meet the needs of high-assurance software development. SPARK is based on Ada, both subsetting the language to remove features that defy verification and also extending the system of contracts by defining new Ada aspects to support modular, constructive, formal verification.
The SPARK Reference Manual is intended as a reference guide for users and implementors of the language. In this context, “implementors” includes those producing both compilers and verification tools.
This is the SPARK Reference Manual for the Community 2020 release of SPARK.