SPARK by Example is a project (greatly) inspired by ACSL by Example, a collection of verified C functions and data types from the C++ standard library. SPARK by Example has two objectives
- implement and verify the same functions as ACSL by Example using SPARK 2014 (SPARK 2014 is a formally verified subset of the Ada programming language)
- highlight differences between verification of C programs and verification of SPARK programs
Adacore has developed a great tutorial website for Ada/SPARK beginners here. It is recommended to follow at least the SPARK part of this tutorial before reading SPARK by Example.
GNAT Community 2018 has been used for this project. You may download and install it using the previous link.
- non mutating algorithms
- maxmin algorithms
- binary search algorithms
- mutating algorithms
- numeric algorithms
- heap algorithms
- sorting algorithms
- classic sorting algorithms
Each directory corresponds to a chapter of ACSL by Example. Each
directory contains a GNAT Project file (the file ending by .gpr)
containing informations about the location of the sources
etc. Common configuration, e.g. GNATprove configuration, is
specified in the spark_by_example_shared.gpr file at the project
root.
For each algorithm Algo to be proved, you will find the
specification of Algo in the algo_p.ads file and its
implementation if the algo_p.adb file. Specifications and
implementations are defined in packages. To avoid name clashes with
functions, packages names have a _P suffixes, hence the file
names.
Ghost functions that may be used in several algorithms are grouped
in the spec directory at the root of the project. Lemmas used in
proofs are grouped in the lemmas directory at the root of the
project.
A Makefile is provided for each chapter with some default values
for provers timeouts, levels of proof etc. These default values are
sufficient to prove the corresponding algorithms with the previous
tools on a machine equipped with an Intel Core i7-4810MQ CPU and
16GB of RAM. For each chapter, a all target proves all functions
and procedures of the chapter. Each function or procedure has a
corresponding target to prove it.
The following variables can be used to control the behaviour of the Makefiles:
CHAPTER_NAME_DEFAULT_TIMEOUT(defined at the beginning of each Makefile) contains the default value for provers timeoutLEVEL_FUNCTION_NAMEdefines for each function the level used byGNATproveMEMCACHED=1enables the use of a Memcached server to cache proofs (it speeds up the proof process as some lemmas are used in several function for instance). VariablesMEMCACHED_SERVERandMEMCACHED_PORTcan be used to specify IP and port of server (localhost:11211by default)STATS=1enables the generation of statistics on the proof, based on the standard output. Generated files will be placed in thestatsdirectory at the root of the projectPARALLELcontrols the-joption ofGNATprovefor parallelizing proofs (default0, use all cores of the machine)DEBUG=1enables debug and verbose options ofGNATprove
Other variables are available, see the Makefile-common file at
the root of the project.
For instance, if you want to prove all functions of chapter on non-mutating algorithms with statistics and by changing the default timeout to 10, issue the following command from the project root:
make -C non-mutating all STATS=1 NON_MUTATING_DEFAULT_TIMEOUT="TIMEOUT=10"A Makefile is also available at the root of the project. It has a
all-chapters target that proves all the chapters, gathers
statistics, and generate a recap.csv file in the stats
directory.
For instance, if you want to prove all chapters with statistics and Memcached, issue the following command:
make all-chapters STATS=1 MEMCACHED=1If you want to contribute to SPARK by Example, please read the CONTRIBUTING file.