GNAT is an implementation of the Ada programming language. SPARK is a restricted subset of Ada for formally verifying programs. It provide features comparable to languages like Rust and ATS. A recent article comparing SPARK to Rust caught my eye and I decided to spend some time learnig Ada and SPARK. This post just outlines installing an implementation of both, a quick test to see if the installation worked, and some things to read to learn. I hope to post more later as I learn more.
Download GNAT GPL from libre.adacore.com. Choose "Free Software or Academic Development" and click "Build Your Download Package". Select the platform and click the checkboxes next to the required components. For my case I chose them all but "GNAT Ada 2016" and "Spark 2016" are the main ones I needed.
To install Ada and SPARK from the downloaded tar file:
$ tar xvf AdaCore-Download-2017-04-27_0537.tar $ cd x86_64-linux/adagpl-2016/gnatgpl $ mkdir ~/ada $ tar -xf gnat-gpl-2016-x86_64-linux-bin.tar.gz $ cd gnat-gpl-2016-x86_64-linux-bin $ ./doinstall ...answer prompts about where to install... ...for this example I used /home/username/gnat... $ export PATH=/home/username/gnat/bin:$PATH $ cd ../sparkgpl $ tar -xf spark-gpl-2016-x86_64-linux-bin.tar.gz $ cd spark-gpl-2016-x86_64-linux-bin $ ./doinstall ...answer prompts about where to install... ...it should pick up the location used above...
Be aware that the install comes with its own
gcc and other utilities. By putting it first in the
PATH they are used over the systems versions.
The following is a "Hello World" application in Ada:
with Ada.Text_IO; use Ada.Text_IO; procedure Hello is begin Put_Line ("Hello World!"); end Hello;
It imports a package,
Ada.Text_IO, and uses it so the package contents can be used without prefixing them with the package name. A procedure called
Hello is created that outlines a line of text. If put in a file
hello.adb it can be compiled with:
$ gnatmake hello.adp gnatbind -x hello.ali gnatlink hello.ali $ ./hello Hello World!
Completely static executables can also be created:
$ gnatmake hello.adb -bargs -static -largs -static $ ldd hello not a dynamic executable $ ./hello Hello World!
I used an example taken from Generating Counterexamples for failed Proofs. The SPARK checker,
gnatproof, requires a project file. This is the contents of
project Saturate is for Source_Dirs use ("."); package Compiler is for Default_Switches ("Ada") use ("-gnatwa"); end Compiler; end Saturate;
It gives the project name,
Saturate, the location to search for source files (the current directory), and any compiler switches. The function to be implemented is a saturation function. It ensures a value given to it is in a specific range. In this case, a non-negative value less than or equal to 255. In file
saturate.ads we put the interface definition:
with Interfaces; use Interfaces; function Saturate (Val : Unsigned_16) return Unsigned_16 with SPARK_Mode, Post => Saturate'Result <= 255 and then (if Val <= 255 then Saturate'Result = Val);
The code first pulls the
Interfaces package into the current namespace. This provides unprefixed access to
Unsigned_16. It declares a function,
Saturate, that takes an
Unsigned_16 as an argument and returns the same type. The
SPARK_Mode is an annotation that identifes code to be checked by SPARK. The
Post portion is a postcondition that the implementation of the function must adhere to. In this case the result must be less than 255 and if the given value is less than 255 then the result will be equal to the value.
The implementation of the function is in a file
function Saturate (Val : Unsigned_16) return Unsigned_16 with SPARK_Mode is begin return Unsigned_16'Max (Val, 255); end Saturate;
This calls the
Max function for
Unsigned_16 types to return the maximum between the given value and 255. The code compiles with the Ada compiler:
$ gnatmake saturate.adb gcc -c saturate.adb
It fails however when running the SPARK checker:
$ gnatprove -Psaturate Phase 1 of 2: generation of Global contracts ... Phase 2 of 2: flow analysis and proof ... saturate.ads:6:11: medium: postcondition might fail (e.g. when Saturate'Result = 255 and Val = 0) Summary logged in gnatprove/gnatprove.out
This tells us that the postcondition might fail if the given value to the function is
0 and the result is
255. This is because we are using
Max - given the value
255. The function result will be
255. The postcondition however states that the result should be equal to val - it should be
0. Changing the function call to
Min fixes it:
$ gnatprove -Psaturate Phase 1 of 2: generation of Global contracts ... Phase 2 of 2: flow analysis and proof ... Summary logged in gnatprove/gnatprove.out
Having a postcondition that states what the result should be is probably unlikely in a lot of code. If the signature was the following, would SPARK find the error still?:
function Saturate (Val : Unsigned_16) return Unsigned_16 with SPARK_Mode, Post => Saturate'Result <= 255 $ gnatprove -Psaturate Phase 1 of 2: generation of Global contracts ... Phase 2 of 2: flow analysis and proof ... saturate.ads:6:11: medium: postcondition might fail, cannot prove Saturate'Result <= 255 (e.g. when Saturate'Result = 256) Summary logged in gnatprove/gnatprove.out
Apparently so. Now it identifies that the result can be 256. Other examples following different contracts on the function are in the original article.
The GNAT User's Guide for Native Platforms and Spark 2014 User's Guide contains the instructions for the main tools. GNAT can interface with C and C++. There is a full list of documentation here. Two useful books covering Ada and Spark:
Some technical papers that give a quick overview of Ada:
I used the command line tools here but there is a
gps command which is a full graphical IDE which may be more approachable. I'm looking forward to using Ada and SPARK and seeing how they compare to tools like Rust and ATS.