program_proofs_in_spark/README.md

Program Proofs in SPARK

This repository contains some programs from Rustan Leino's excellent book "Program Proofs" verified with SPARK.

All examples in branch master prove at level 2 (using switch --level=2) using SPARK Pro 23.

All examples in branch fsf prove at level 2 (using switch --level=2) using SPARK FSF, that you can download directly or through Alire following the instructions on the README of the SPARK project.

Compared to SPARK Pro 23, the current FSF release does not include yet:

• structural loop and subprogram variants

• loop and subprogram variants on Big_Natural

• the new organization of SPARKlib

• annotation Automatic_Instantiation

If you want to contribute another example, please open a PR with the code, following the organization of existing chapters, with a project file per chapter. Missing examples of interest are:

• the list operation of chapter 6

• insertion sort and merge sort from chapter 8

• the queue of chapter 9

• the priority queue of chapter 10

• the sums of chapter 12

• linear search and binary search of chapter 13

• the array operations of chapter 14

• the objects with invariants of chapter 16

• the objects with dynamic allocation of chapter 17

For many of these, inspiration from similar examples can be found in the examples presented in the SPARK User's Guide.