Gem #69: Let's SPARK! — Part 2
by Yannick Moy —AdaCore
Let's get started…
In the last Gem, we proved that procedure Linear_Search was free from uninitialized variable accesses and run-time errors, which are safety properties of Linear_Search.
Now we can try to prove a specific behavioral property of Linear_Search, expressed as a contract between Linear_Search and its callers. A contract will consist of a precondition that callers of Linear_Search are responsible for establishing, before calling Linear_Search, and a postcondition that Linear_Search must establish, before returning to the caller. If not present, a default "true" pre- or postcondition is assumed.
Let's prove that when Linear_Search returns with Found = True, the value of Table at Index is Value. This can be expressed in SPARK as a postcondition on procedure Linear_Search that is located after its declaration in search.ads:
procedure Linear_Search
(Table : in IntArray;
Value : in Integer;
Found : out Boolean;
Index : out Integer);
--# post Found -> Table(Index) = Value;
Notice the implication symbol ->, which is only defined in SPARK annotations.
Let's call the SPARK tools, as we did in the previous Gem: Examine, Simplify All, POGS ...
This time, the column "TO DO" is not empty:
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 | rtc check @ 14 | | YES | | | | |
6 | 13 | rtc check @ 16 | | YES | | | | |
7 | 13 | assert @ finish | | YES | | | | |
8 | 13 | assert @ finish | | | | | | YES |
---------------------------------------------------------------------------
If we right-click on this line and select SPARK/Show Simplified VC, GPS opens a file linear_search.siv, which shows that the unproved VC corresponds precisely to the postcondition we just added:
C1: found -> element(table, [index]) = value .
This is the conclusion (C) that the prover tries to prove with the set of hypotheses (H) above it. If we look at the hypotheses, we see that the conclusion cannot indeed be proved. This has to do with the warning which we already saw in the previous Gem:
Warning 402 - Default assertion planted to cut the loop
To prove a property of a procedure with a loop, we cannot unroll the loop an unbounded number of times. Therefore, SPARK "cuts" the loop with a loop invariant, which is a property that the loop maintains. Unless you provide such a loop invariant, SPARK assumes by default that nothing is maintained through the loop. If you provide one, SPARK will prove three things:
1) the loop invariant holds when control enters the loop for the first time
2) the loop invariant is maintained during an arbitrary run through the loop
3) the loop invariant is sufficient to prove the postcondition
What is missing in our case is the information that Found remains False throughout the loop. Let's add it, with the following syntax in search.adb:
for I in Integer range Table'Range loop
--# assert Found = False;
Let's do it again: Examine, Simplify All, POGS ...
Notice that the warning about a default assertion disappeared.
This time, the "TO DO" column is empty, so we have successfully proved Linear_Search's postcondition!
Finally, let's see how SPARK deals with global variables, by adding a counter to Linear_Search, which is incremented by one each time the call succeeds. We need to state explicitly that Counter is part of the state of this package, which we do using an "own" annotation below. We also need to state explicitly that Counter is initialized using an "initializes" annotation. The following declaration should go into search.ads:
package Search
--# own Counter;
--# initializes Counter;
is
Counter : Natural := 0;
Now, we increment Counter in Linear_Search's body in search.adb:
if Table(I) = Value then
Counter := Counter + 1;
If we try to run the Examiner at this point, it flags an error:
Semantic Error 1 - The identifier Counter is either undeclared or not
visible at this point
This is because reads and writes of global variables are part of a subprogram specification in SPARK. Since Linear_Search does not declare in its specification that it reads or writes a global variable, it is not allowed to do so in its body. So let's add a SPARK annotation to state that Linear_Search reads and writes Counter.
procedure Linear_Search
(Table : in IntArray;
Value : in Integer;
Found : out Boolean;
Index : out Integer);
--# global in out Counter;
--# post Found -> Table(Index) = Value;
Let's do it again: Examine, Simplify All, POGS ...
We get a new unproved VC in the column "TO DO", which corresponds to the following conclusion:
C1: counter <= 2147483646 .
This time, it is because SPARK has detected a problem during the proof that the update of Counter does not overflow. Indeed, it could overflow! The solution is to add a precondition to Linear_Search, that promises that it will never be called in a state where Counter is the largest integer value.
procedure Linear_Search
(Table : in IntArray;
Value : in Integer;
Found : out Boolean;
Index : out Integer);
--# global in out Counter;
--# pre Counter < Integer'Last;
--# post Found -> Table(Index) = Value;
As before, we must modify the loop invariant. Here, we just have to repeat this information in the loop invariant:
for I in Integer range Table'Range loop
--# assert Found = False and Counter < Integer'Last;
Let's do it again: Examine, Simplify All, POGS ...
Everything is proved!
Notice that the promise made by the precondition will have to be proved by callers of Linear_Search ...
Finally, let's add to the SPARK annotation of Linear_Search that Counter is incremented by one when Linear_Search returns Found = True. This can be expressed as a postcondition relating the value of Counter at procedure entry, denoted Counter~, and the value of Counter at procedure exit, denoted Counter:
procedure Linear_Search
(Table : in IntArray;
Value : in Integer;
Found : out Boolean;
Index : out Integer);
--# global in out Counter;
--# pre Counter < Integer'Last;
--# post Found -> (Table(Index) = Value and Counter = Counter~ + 1);
Notice that in the precondition we simply use Counter to denote the value at procedure entry, because the precondition is precisely evaluated at procedure entry.
As before, we update the loop invariant to state that the current value of Counter is the same as the one at procedure entry:
for I in Integer range Table'Range loop
--# assert Found = False and Counter < Integer'Last
--# and Counter = Counter~;
Let's do it a last time: Examine, Simplify All, POGS ...
Everything is proved!
Remember though that we can only prove a contract we wrote, which may be very different from saying abstractly that procedure Linear_Search is "correct". Who knows what the correct behaviour of Linear_Search means for the human who programmed it?
Let's recap what we have seen so far. SPARK is a language that combines a strict subset of Ada with annotations written inside stylized Ada comments. We have seen various kinds of SPARK annotations: preconditions introduced by pre; postconditions introduced by post; loop invariants introduced by assert; frame conditions introduced by global, own, and initializes. The SPARK tools allow us to check that a procedure is free from uninitialized variable accesses, that it executes without run-time errors, and that it respects a given contract, written next to its declaration, that callers can rely on.
In later Gems we will explore in more depth the capabilities of SPARK and its integration with GPS. In the meantime, you can learn more about SPARK in the SPARK tutorial at http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/.
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.