This chapter provides an overview of the SPARK 2014 language, detailing for each feature its consequences in terms of execution and formal verification. This is not a reference manual for the SPARK 2014 language, which can be found in:
More details on how GNAT Pro compiles SPARK 2014 code can be found in the GNAT Pro Reference Manual.
To facilitate formal verification, SPARK 2014 enforces a number of global simplifications to Ada 2012. The most notable simplifications are:
Uses of these features in SPARK 2014 code are detected by GNATprove and reported as errors. Formal verification is not possible on subprograms using these features.
We describe a program unit or language feature as being “in SPARK 2014” if it complies with the restrictions required to permit formal verification. Conversely, a program unit language feature is “not in SPARK 2014” if it does not meet these requirements, and so is not amenable to formal verification. Within a single unit, features which are “in” and “not in” SPARK 2014 may be mixed at a fine level. For example, the following combinations may be typical:
Such patterns are intended to allow for application of formal verification to a subset of a program, and the combination of formal verification with more traditional testing (see Combining Formal Verification and Testing).
This pragma is used to designate whether a contract and its implementation must follow the SPARK 2014 programming language syntactic and semantic rules. The pragma is intended for use with formal verification tools and has no effect on the generated code. Its syntax is:
pragma SPARK_Mode [ (On | Off | Auto) ] ;
When used as a configuration pragma over a whole compilation or in a particular compilation unit, it sets the mode of the units involved, in particular:
Pragma SPARK_Mode can be used as a local pragma with the following semantics:
In code where SPARK_Mode applies, any violation of SPARK 2014 is reported by GNATprove as an error, and any construct in SPARK 2014 not yet implemented is reported as a warning.
SPARK 2014 contains many features for specifying the intended behavior of programs. Some of these features come from Ada 2012 (preconditions and postconditions for example). Other features are specific to SPARK 2014 (loop invariants and variants for example). In this section, we describe these features and their impact on execution and formal verification.
Preconditions and postconditions are the most important annotations in SPARK 2014. They specify the contract of a subprogram. For example:
1 2 3 | procedure Incr_Threshold (X : in out Integer) with
Pre => X >= 0,
Post => X = Integer'Min (X'Old + 1, Threshold);
|
The precondition states the obligation on the caller of the subprogram. For example, all callers of Incr_Threshold should ensure that the value passed in parameter is non-negative before calling Incr_Threshold. The postcondition states the obligation on the subprogram when it returns. For example, Incr_Threshold should always return in a state where the value of its parameter is the minimum between its value at entry (X'Old) incremented by one, and a given threshold value. This expresses precisely the property of incrementing until a threshold is reached.
The special attributes Result and Old defined in Ada 2012 are allowed in postconditions only (not in preconditions), to refer respectively to the result of a function, and the value of an object on subprogram entry.
When compiling with assertions (switch -gnata in GNAT Pro), the resulting program contains run-time checks that the precondition evaluates to True on subprogram entry, and that the postcondition evaluates to True on subprogram exit. Their evaluation should also not raise a run-time error, for example when accessing an array element, or doing arithmetic computations.
When proving a subprogram with GNATprove, its precondition is assumed to hold, and its postcondition is proved. GNATprove also generate checks to prove that the precondition can never raise a run-time error, whatever the calling context. For example:
1 2 3 4 5 6 7 | function Add (X, Y : Integer) return Integer with
Pre => X + Y in Integer,
Post => Add'Result = X + Y;
function Access (A : My_Array; J : Index) return Element with
Pre => A(J) /= No_Element,
Post => Add'Result = A(J);
|
GNATprove generates checks to show that X + Y in the precondition of Add can never overflow, and that A(J) in the precondition of Access can never access A outside its bounds. These checks cannot be proved. One can usually rewrite the precondition so that it cannot raise a run-time error, either by adding a guard in the precondition, or by using a different formulation that cannot raise a run-time error. For example:
1 2 3 4 5 6 7 8 | function Add (X, Y : Integer) return Integer with
Pre => (if X > 0 and Y > 0 then X <= Integer'Last - Y)
and then (if X < 0 and Y < 0 then X >= Integer'First - Y),
Post => Add'Result = X + Y;
function Access (A : My_Array; J : Index) return Element with
Pre => J in A'Range and then A(J) /= No_Element,
Post => Add'Result = A(J);
|
For overflow checks, an alternate solution exists to avoid them altogether in annotations, by using unbounded arithmetic in annotations, see Overflow Modes.
A correct contract may not be sufficient for proof: even if the precondition and postcondition always evaluate to True, and never raise a run-time error, they might not be strong enough:
One can strengthen a contract by making its precondition more restrictive (accepting less calling contexts) and making its postcondition more precise (giving more information to prove its callers).
Note that the default precondition (resp. postcondition) of True used by GNATprove when no explicit one is given may not be strong enough.
Note also that direct recursive subprograms or mutually recursive subprograms are treated in this respect exactly like non-recursive ones. Provided the execution of these subprograms always terminates (a property that is not verified by GNATprove), then it is sound to use their contracts at call-site to prove the same contracts.
The contract of a subprogram can alternatively be specified as a set of disjoint and complete contract cases:
1 2 3 | procedure Incr_Threshold (X : in out Integer) with
Contract_Cases => (X < Threshold => X = X'Old + 1,
X >= Threshold => X = X'Old);
|
Each case in the list consists in a guard and a consequence separated by the symbol =>. All guards are evaluated on entry to the subprogram. For each input, only one guard should evaluate to True. The corresponding consequence should evaluate to True when returning from the subprogram. For example, the contract cases of Incr_Threshold expresses that the subprogram should be called in two distinct cases only:
Contract cases provide a convenient way to express complex contracts, which would be cumbersome to express with a precondition and a postcondition. For example, the contract cases of Incr_Threshold are equivalent to the following precondition and postcondition:
1 2 3 4 5 | procedure Incr_Threshold (X : in out Integer) with
Pre => (X < Threshold and not (X = Threshold))
or else (not (X < Threshold) and X = Threshold),
Post => (if X'Old < Threshold'Old then X = X'Old + 1
elsif X'Old = Threshold'Old then X = X'Old);
|
Note that using contract cases or the equivalent (for run-time checking) preconditions and postconditions is not equivalent for proof with GNATprove. If contract cases are used, GNATprove attempts to prove that they are disjoint and complete once and for all. If preconditions and postconditions are used, GNATprove treats these properties as any other precondition, so they must be verified at each call.
Contract cases can also be used in addition to preconditions and postconditions. In that case, the cases should cover all inputs allowed by the precondition. For example, the contract of Incr_Threshold can be written:
1 2 3 4 5 | procedure Incr_Threshold (X : in out Integer) with
Pre => X in 0 .. Threshold,
Post => X >= X'Old,
Contract_Cases => (X < Threshold => X = X'Old + 1,
X = Threshold => X = X'Old);
|
GNATprove is able to prove that the contract cases of Incr_Threshold are disjoint and complete, even if the case of X greater than Threshold is not considered, because this case is ruled out by the precondition of Incr_Threshold.
Note that the completeness is automatically reached when the last guard is others, denoting all cases not captured by any of the other guard. For example:
1 2 3 4 | procedure Incr_Threshold (X : in out Integer) with
Contract_Cases => (X >= 0 and X < Threshold => X = X'Old + 1,
X = Threshold => X = X'Old,
others => X = -1;
|
Expression functions that do not have a user-defined postcondition are treated specially by GNATprove, which generates an implicit postcondition stating that their result is equal to the expression that defines them. For example, the function Increment defined as an expression function:
function Increment (X : Integer) return Integer is (X + 1);
is treated by GNATprove as if it had a postcondition:
Post => Increment'Result = X + 1;
This postcondition is automatically satisfied, so GNATprove does not generate checks for it. Expression functions that have a user-defined postcondition are treated like regular functions.
The contracts of functions called in annotations are essential for automatic proofs. Currently, the knowledge that a function call in an annotation respects its postcondition (when called in a context where the precondition is satisfied) is only available for expression functions. Thus, expression functions should be used whenever possible for these functions called in annotations. The syntax of expression functions, introduced in Ada 2012, allows defining functions whose implementation simply returns an expression, such as Is_Even, Is_Odd and Is_Prime below.
1 2 3 4 5 6 | function Is_Even (X : Integer) return Boolean is (X mod 2 = 0);
function Is_Odd (X : Integer) return Boolean is (not Even (X));
function Is_Prime (X : Integer) with
Pre => Is_Odd (X);
|
The standard library for the host is pre-analyzed, and Global contracts are generated for these subprograms, so that user code can call standard library subprograms.
In order for GNATprove to prove formally the properties of interest on subprograms with loops, the user should annotate these loops with loop invariants. A loop invariant gives information on the state at entry to the loop at each iteration. Loop invariants in SPARK 2014 are expressed with the Loop_Invariant pragma, which may appear anywhere in the main list of statements in a loop body, or directly in a chain of nested block statements in this main list of statements. Only the first Loop_Invariant pragmas are used by GNATprove as a loop invariant during proof (they should be next to each other, or separated only by Loop_Variant pragmas). GNATprove considers internally the virtual loop formed around these loop invariants to prove the subprogram. Other Loop_Invariant pragmas are proved like regular assertions. Loop invariants may have to be precise enough to prove the property of interest. For example, in order to prove the postcondition of function Contains below, one has to write a precise loop invariant such as the one given below:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 | function Contains (Table : IntArray; Value : Integer) return Boolean with
Post => (if Contains'Result then
(for some J in Table'Range => Table (J) = Value)
else
(for all J in Table'Range => Table (J) /= Value));
function Contains (Table : IntArray; Value : Integer) return Boolean is
begin
for Index in Table'Range loop
pragma Loop_Invariant (for all J in Table'First .. Index - 1 =>
Table (J) /= Value);
if Table(Index) = Value then
return True;
end if;
end loop;
return False;
end Contains;
|
When the loop involves modifying a variable, it may be necessary to refer to the value of the variable at loop entry. This can be done using the GNAT attribute Loop_Entry. For example, in order to prove the postcondition of function Move below, one has to write a loop invariant referring to Src'Loop_Entry such as the one given below:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | procedure Move (Dest, Src : out IntArray) with
Post => (for all J in Dest'Range => Dest (J) = Src'Old (J));
procedure Move (Dest, Src : out IntArray) is
begin
for Index in Dest'Range loop
pragma Loop_Invariant ((for all J in Dest'First .. Index - 1 =>
Dest (J) = Src'Loop_Entry (J))
and then
(for all J in Index .. Dest'Last =>
Src (J) = Src'Loop_Entry (J)));
Dest (Index) := Src (Index);
Src (Index) := 0;
end loop;
end Move;
|
Note in particular the second conjunct in the loop invariant, which states that the Src array has not been modified between indexes Index and Dest'Last. This part of an invariant or contract stating what has not been modified, called in the literature the frame condition, is essential for GNATprove to work effectively. Special care should be taken to write adequate frame conditions, as they usually look obvious to programmers, and so it is very common to forget to write them.
Proofs of termination of loops rely on Loop_Variant pragmas. Proving one loop variant is sufficient to prove that a loop terminates, even if the loop contains multiple Loop_Variant pragmas, and others are not proved. Indeed, it is sufficient to know that one bounded quantity decreases or increases monotonically (or a mix of these, as loop invariants may have increasing and decreasing parts, the order of which fixes the lexicographic combined order of progress) to be assured that the loop terminates. Note that, in general, this requires proving also that there are no run-time errors in the loop, to show that the quantity stays within bounds. Otherwise, the code may still wrap around at run time (if the code is compiled without checks), and the loop will not necessarily exit.
The Loop_Variant pragmas that appear next to the first group of Loop_Invariant pragmas (or at the start of the loop body if there are no Loop_Invariant pragmas in the loop) are handled with the most precision by GNATprove, as they become loop variants of the underlying virtual loop. Other Loop_Variant pragmas are proved by showing that the quantity that should progress monotonically does so between the program point where the first group of Loop_Invariant pragmas appears (or the start of the loop if there is no such group) and the program point where the Loop_Variant pragma appears, and that this quantity either stays the same or progresses on the rest of the loop.
Ada 2012 quantified expressions are a special case with respect to run-time errors: the enclosed expression must be run-time error free over the entire range of the quantification, not only at points that would actually be reached at execution. As an example, consider the following expression:
(for all I in 1 .. 10 => 1 / (I - 3) > 0)
This quantified expression will never raise a run-time error, because the test is already false for the first value of the range, I = 1, and the execution will stop, with the result value False. However, GNATprove requires the expression to be run-time error free over the entire range, including I = 3, so there will be an unproved VC for this case.
GNATprove may need to consider many possible paths through a subprogram. If this number of paths is too large, GNATprove will take a long time to prove even trivial properties. To reduce the number of paths analyzed by GNATprove, one may use the pragma Assert_And_Cut, to mark program points where GNATprove can cut paths, replacing precise knowledge about execution before the program point by the assertion given. The effect of this pragma for compilation is exactly the same as the one of pragma Assert.
For example, in the procedure below, all that is needed to prove that the code using X is free from run-time errors is that X is positive. Without the pragma, GNATprove considers all execution paths through P, which may be many. With the pragma, GNATprove only needs to consider the paths from the start of the procedure to the pragma, and the paths from the pragma to the end of the procedure, hence many fewer paths.
1 2 3 4 5 6 7 | procedure P is
X : Integer;
begin
-- complex computation that sets X
pragma Assert_And_Cut (X > 0);
-- complex computation that uses X
end P;
|
1 2 3 | function Add (X, Y : Integer) return Integer with
Pre => X + Y in Integer,
Post => Add'Result = X + Y;
|
Containers are generic data structures offering a high-level view of collections of objects, while guaranteeing fast access to their content to retrieve or modify it. The most common containers are lists, vectors, sets and maps, which are defined in Ada Standard Libraries. In critical software where verification objectives severely restrict the use of pointers, containers offer an attractive alternative to pointer-intensive data structures.
There are 6 formal containers: Formal_Vectors, Formal_Doubly_Linked_Lists, Formal_Hashed_Sets, Formal_Ordered_Sets, Formal_Hashed_Maps, and Formal_Ordered_Maps. They are adapted to critical software development. They are bounded, so that there can be no dynamic allocation and they have preconditions that can be used to ensure that there is no error at run-time. They are experimental, and, as such, should be used with care. In particular, the examples below can be compiled and fed to GNATprove but not everything is proved about them in a reasonable amount of time.
Specification of formal containers is in SPARK 2014. As a consequence, there is no procedure that take a procedure as an argument such that Update_Element or Query_Element in Ada Standard container library. What is more, the Ada 2012 iteration mechanism that allows the use of for all and for some on Ada Standard containers is not available on formal containers.
Formal containers are adapted to the specification process. First of all, cursors no longer have a reference to underlying container. Indeed, in Ada Standard container library, cursor contain a pointer to their underlying container. As a consequence, if a container is modified then so are every cursor of this container. This modification also allows to use the same cursor inside different containers. In particular, it is useful to link elements associated to a list before and after a modification. Formal containers also provide three new functions per container type. Right (C : Container; Cu : Cursor) returns Container and Left (C : Container; Cu : Cursor) returns Container can be used to write loop invariant. They return the right (resp. the left) part of the container C starting before (resp. stopping before) the cursor Cu.
For example, in the function My_Find below, Left is used in the loop-invariant to state that the element E has not been found in the part of the list that as been analyzed yet.
1 2 3 4 5 | function My_Find (L : List; E : Element_Type) return Cursor with
Post => (if My_Find'Result = No_Element then
not Contains (L, E)
else Has_Element (L, My_Find'Result) and then
Element (L, My_Find'Result) = E);
|
1 2 3 4 5 6 7 8 9 10 11 12 | function My_Find (L : List; E : Element_Type) return Cursor is
Cu : Cursor := First (L);
begin
while Has_Element (L, Cu) loop
pragma Loop_Invariant (not Contains (Left (L, Cu), E));
if Element (L, Cu) = E then
return Cu;
end if;
Next (L, Cu);
end loop;
return No_Element;
end My_Find;
|
The third new function, Strict_Equal (C1, C2 : Container) checks whether C1 and C2 really are equal with respect to everything that can impact existing functions of the library. On lists for example, it does not only check that C1 and C2 contain the same elements in the same order but also that C1 and C2 share the same cursors. This function is generaly used for writing frame-conditions.
For example, in the function My_Preppend below, Strict_Equal is used to state that My_Preppend does not modify the tail of the list. Note that we use First (L1'Old) to refer to the first element of the tail in the output of preppend, which would not have been possible is cursors still had an internal reference to the list they come from.
1 2 3 4 5 | procedure My_Preppend (L1 : in out List; E : Element_Type) with
Pre => L1.Capacity > Length (L1),
Post => Length (L1) = 1 + Length (L1'Old) and then
First_Element (L1) = E and then
Strict_Equal (Right (L1, First (L1'Old)), L1'Old);
|