SPARK by Example
GitHub - tofgarion/spark-by-example: SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
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

  non mutating algorithms
  maxmin algorithms
  binary search algorithms
  mutating algorithms
  numeric algorithms
  heap algorithms
  sorting algorithms
  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

