Gem #68: Let's SPARK! — Part 1
by Yannick Moy —AdaCore
Let's get started…
With Altran and AdaCore now teaming up to offer an integration of SPARK technology inside GPS (see http://www.adacore.com/home/products/sparkpro/), many GPS users will be interested in trying out the proof capabilities of SPARK on their own Ada programs. Of course it's a little more involved than that. SPARK is not only a set of tools for verifying high-assurance systems, but also incorporates a language that must be learned.
The SPARK language is made up of two parts, one of which is a subset of Ada (whose features will obviously already be familiar to Ada programmers!), meant to facilitate code understanding and proofs, and the other part being a specification language, meant to express properties of programs. Quite conveniently, the SPARK specifications (a.k.a. SPARK annnotations, to distinguish them from Ada specifications) are expressed within stylized Ada comments of the following form:
--# so SPARK annotations don't interfere with normal Ada compilation.
This Gem and the next one demonstrate various of the properties you can prove with SPARK, and how these relate to the SPARK annotations written by the user. As a simple example, we will take a procedure which searches linearly for a value in an array, and returns the index, if any, at which the value is found.
Here is the specification file search.ads:
package Search is
type IntArray is array (Integer range <>) of Integer;
procedure Linear_Search
(Table : in IntArray;
Value : in Integer;
Found : out Boolean;
Index : out Integer);
end Search;
And the body file search.adb:
package body Search is
procedure Linear_Search
(Table : in IntArray;
Value : in Integer;
Found : out Boolean;
Index : out Integer)
is
I : Integer := 0;
begin
Found := False;
while I <= Table'Last loop
if Table(I) = Value then
Found := True;
Index := I;
exit;
end if;
I := I + 1;
end loop;
end Linear_Search;
end Search;
Let's first get set up for using SPARK:
1. Copy the files search.ads and search.adb into a directory named search.
2. Open GPS with a default project in the same directory.
3. Expand file search.adb.
4. Select SPARK/SPARKMake from the menu. This generates a file search.idx.
5. Copy the following code to a file called search.cfg:
package Standard is
type Integer is range -2**31 .. 2**31-1;
end Standard;
6. From the Menu, select Project/Edit Project Properties.
7. Go to the page Switches/Examiner.
8. Select the following options:
Index File : search.idx Configuration File : search.cfg Analysis : Data Flow only Generate VCs : yes (check it)
That's it!
Now open search.adb and select SPARK/Examine File. The SPARK Examiner runs and outputs the following messages:
Flow Error 602 - The undefined initial value of Index may be
used in the derivation of Index
Warning 402 - Default assertion planted to cut the loop
Note - Information flow analysis not carried out
The Flow Error indicates that, although Index is an out parameter, it is not initialized on all paths through Linear_Search. One could argue that our intent here is to access Index only when Found is set to True. SPARK considers initialization errors too serious to allow such subtleties, and requires that all paths through the procedure must initialize all out parameters. Let's comply and initialize Index:
begin
Found := False;
Index := 0;
After we rerun the Examiner, we are left with a Note that is simply a reminder of our choice of options, and a Warning that we will explain in the next Gem.
Now, we can continue with proving that our procedure is free from run-time errors, such as integer overflow and out-of-bounds array accesses. Select SPARK/Simplify All. The SPARK Simplifier runs. To see the result of this tool's execution, select SPARK/POGS. This opens a file search.sum, which summarizes all the proofs in the following table:
VCs for procedure_linear_search :
----------------------------------------------------------------------------
| | | -----Proved In----- | | |
# | From | To | vcg | siv | plg | prv | False | TO DO |
----------------------------------------------------------------------------
1 | start | rtc check @ 13 | | YES | | | | |
2 | start | assert @ 15 | | YES | | | | |
3 | 15 | assert @ 15 | | YES | | | | |
4 | 15 | rtc check @ 16 | | | | | | YES |
5 | 15 | rtc check @ 18 | | YES | | | | |
6 | 15 | rtc check @ 21 | | | | | | YES |
7 | 15 | assert @ finish | YES | | | | | |
8 | 15 | assert @ finish | YES | | | | | |
----------------------------------------------------------------------------
Each line corresponds to a Verification Condition (VC), which must be proved in order to guarantee that the program is free from run-time errors. Each column corresponds to the result of the proof attempt. If YES appears in one of the 4 "Proved In" columns, the proof was successful. If YES appears in the "False" column, there is something definitely wrong. If "YES" appears in the "TO DO" column, we don't know: either the program is wrong, or it is too complex to prove.
Since column "TO DO" is not empty here, not all proofs were successful. In the next Gem, we will give you more details about failed proofs. The reason for the failures here is that program Linear_Search is incorrect, meaning that run-time errors can be raised. To see this, just complete the program with the following code in main.adb, and build the executable.
with Search; use Search; procedure Main is Table : IntArray(1..10) := (others => 0); Found : Boolean; Index : Integer; begin Linear_Search(Table, 0, Found, Index); end Main;
Now run the executable, and it raises an exception:
raised CONSTRAINT_ERROR : search.adb:16 index check failed
This is because we are passing an array to Linear_Search that starts at index 1 in its parameter Table, whereas Linear_Search loop assumes that the array starts at index 0. SPARK correctly assumes that we can pass in such an array to Linear_Search, and thus it fails to prove that Linear_Search is free from run-time errors.
Let's correct the code of Linear_Search:
procedure Linear_Search
(Table : in IntArray;
Value : in Integer;
Found : out Boolean;
Index : out Integer) is
begin
Found := False;
Index := 0;
for I in Integer range Table'Range loop
if Table(I) = Value then
Found := True;
Index := I;
exit;
end if;
end loop;
end Linear_Search;
Let's do it again: Examine, Simplify All, POGS ...
This time, columns "False" and "TO DO" are empty, meaning that all proofs were successful.
VCs for procedure_linear_search :
----------------------------------------------------------------------------
| | | -----Proved In----- | | |
# | From | To | vcg | siv | plg | prv | False | TO DO |
----------------------------------------------------------------------------
1 | start | rtc check @ 11 | | YES | | | | |
2 | start | rtc check @ 13 | | YES | | | | |
3 | start | assert @ 13 | | YES | | | | |
4 | 13 | assert @ 13 | | YES | | | | |
5 | 13 | assert @ 13 | | YES | | | | |
6 | 13 | rtc check @ 14 | | YES | | | | |
7 | 13 | rtc check @ 16 | | YES | | | | |
8 | 13 | assert @ finish | YES | | | | | |
9 | 13 | assert @ finish | YES | | | | | |
----------------------------------------------------------------------------
Thus, we have proved that procedure Linear_Search is free from run-time errors.
In the next Gem, after the summer break, we will prove that procedure Linear_Search actually respects a given contract.
About the Author
Yannick Moy’s work focuses on software source code analysis, mostly to detect bugs or verify safety/security properties. Yannick previously worked for PolySpace (now The MathWorks) where he started the project C++ Verifier. He then joined INRIA Research Labs/Orange Labs in France to carry out a PhD on automatic modular static safety checking for C programs. Yannick joined AdaCore in 2009, after a short internship at Microsoft Research.
Yannick holds an engineering degree from the Ecole Polytechnique, an MSc from Stanford University and a PhD from Université Paris-Sud. He is a Siebel Scholar.