SPARK by Example

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.

Tools used

GNAT Community 2018 has been used for this project. You may download and install it using the previous link.

Table of contents

1. non mutating algorithms
2. maxmin algorithms
3. binary search algorithms
4. mutating algorithms
5. numeric algorithms
6. heap algorithms
7. sorting algorithms
8. classic sorting algorithms

Content of each directory and global Makefile

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 timeout
• LEVEL_FUNCTION_NAME defines for each function the level used by GNATprove
• MEMCACHED=1 enables 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). Variables MEMCACHED_SERVER and MEMCACHED_PORT can be used to specify IP and port of server (localhost:11211 by default)
• STATS=1 enables the generation of statistics on the proof, based on the standard output. Generated files will be placed in the stats directory at the root of the project
• PARALLEL controls the -j option of GNATprove for parallelizing proofs (default 0, use all cores of the machine)
• DEBUG=1 enables debug and verbose options of GNATprove

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=1

Contributing

If you want to contribute to SPARK by Example, please read the CONTRIBUTING file.

References

• SPARK 2014 user guide 19.0
• learn.adacore.com