Basalt is a collection of formally verified building blocks written in SPARK. It is standalone and requires only few runtime features (Interfaces, Secondary Stack). All modules are proven to contain no runtime errors. Furthermore some useful functional properties have been formally verified.
- Basalt.Queue - A FIFO queue implementation. The interface is designed in a way that allows to prove properties about the quantity of elements in the queue.
- Basalt.Stack - A stack implementation. The interface is designed in a way that allows to prove properties about the quantity of elements on the stack.
- Basalt.Slicer - A tool that splits ranges into maximum sized slices. Each slice proves to be in the initially given range and to be at maximum of the given size.
- Basalt.Strings - A collection of String operations.
Currently these are formally proven
Imagefunctions, similar to'Image. The difference is that these image function provide maximum lengths of their output as proof properties. - Basalt.Strings_Generic - The generic variant
of
Stringsfor modular and ranged types.
Basalt itself does not have any further requirements than an Ada runtime with
- Interfaces
- Secondary stack
The componolit-runtime is sufficient to use it.
The recommended compiler is the GNAT Community 2019 Ada compiler that also comes with Aunit and SPARK 2014 to run the tests and and perform the proofs.
Build with
$ gprbuild -P basalt.gpr
To run the Aunit tests run
$ gprbuild -P test/aunit/test.gpr
$ ./test/aunit/obj/test
To perform the proofs run
$ gnatprove -P test/proof/proof.gpr --level=2