2017-04-27
Installing GNAT and SPARK GPL Editions
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.
Installation
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.
Testing GNAT
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!
Testing SPARK
I used an example taken from Generating Counterexamples for failed Proofs. The SPARK checker, gnatproof, requires a project file. This is the contents of saturate.gpr:
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 saturate.adb:
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 0 to Saturate, the Max of 0 and 255 is 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.
Documentation
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.
