Proof of Functional Correctness
This section is dedicated to the functional correctness of programs. It presents advanced proof features that you may need to use for the specification and verification of your program's complex properties.
Beyond Program Integrity
When we speak about the correctness of a program or subprogram, we mean the extent to which it complies with its specification. Functional correctness is specifically concerned with properties that involve the relations between the subprogram's inputs and outputs, as opposed to other properties such as running time or memory consumption.
For functional correctness, we usually specify stronger properties than those required to just prove program integrity. When we're involved in a certification processes, we should derive these properties from the requirements of the system, but, especially in non-certification contexts, they can also come from more informal sources, such as the program's documentation, comments in its code, or test oracles.
For example, if one of our goals is to ensure that no runtime error is
raised when using the result of the function Find below, it may be
enough to know that the result is either 0 or in the range of A. We can
express this as a postcondition of Find.
package Show_Find is
type Nat_Array is array (Positive range <>) of Natural;
function Find (A : Nat_Array; E : Natural) return Natural with
Post => Find'Result in 0 | A'Range;
end Show_Find;
package body Show_Find is
function Find (A : Nat_Array; E : Natural) return Natural is
begin
for I in A'Range loop
if A (I) = E then
return I;
end if;
end loop;
return 0;
end Find;
end Show_Find;
In this case, it's automatically proved by GNATprove.
However, to be sure that Find performs the task we expect, we may want
to verify more complex properties of that function. For example, we want to
ensure it returns an index of A where E is stored and returns 0
only if E is nowhere in A. Again, we can express this as a
postcondition of Find.
package Show_Find is
type Nat_Array is array (Positive range <>) of Natural;
function Find (A : Nat_Array; E : Natural) return Natural with
Post =>
(if (for all I in A'Range => A (I) /= E)
then Find'Result = 0
else Find'Result in A'Range and then A (Find'Result) = E);
end Show_Find;
package body Show_Find is
function Find (A : Nat_Array; E : Natural) return Natural is
begin
for I in A'Range loop
if A (I) = E then
return I;
end if;
end loop;
return 0;
end Find;
end Show_Find;
This time, GNATprove can't prove this postcondition automatically, but
we'll see later that we can help GNATprove by providing a loop invariant,
which is checked by GNATprove and allows it to automatically prove the
postcondition for Find.
Writing at least part of your program's specification in the form of contracts has many advantages. You can execute those contracts during testing, which improves the maintainability of the code by detecting discrepancies between the program and its specification in earlier stages of development. If the contracts are precise enough, you can use them as oracles to decide whether a given test passed or failed. In that case, they can allow you to verify the outputs of specific subprograms while running a larger block of code. This may, in certain contexts, replace the need for you to perform unit testing, instead allowing you to run integration tests with assertions enabled. Finally, if the code is in SPARK, you can also use GNATprove to formally prove these contracts.
The advantage of a formal proof is that it verifies all possible execution
paths, something which isn't always possible by running test cases. For
example, during testing, the postcondition of the subprogram Find shown
below is checked dynamically for the set of inputs for which Find is
called in that test, but just for that set.
package Show_Find is
type Nat_Array is array (Positive range <>) of Natural;
function Find (A : Nat_Array; E : Natural) return Natural with
Post =>
(if (for all I in A'Range => A (I) /= E)
then Find'Result = 0
else Find'Result in A'Range and then A (Find'Result) = E);
end Show_Find;
package body Show_Find is
function Find (A : Nat_Array; E : Natural) return Natural is
begin
for I in A'Range loop
if A (I) = E then
return I;
end if;
end loop;
return 0;
end Find;
end Show_Find;
with Ada.Text_IO; use Ada.Text_IO;
with Show_Find; use Show_Find;
procedure Use_Find with
SPARK_Mode => Off
is
Seq : constant Nat_Array (1 .. 3) := (1, 5, 3);
Res : Natural;
begin
Res := Find (Seq, 3);
Put_Line ("Found 3 in index #" & Natural'Image (Res) & " of array");
end Use_Find;
However, if Find is formally verified, that verification checks its
postcondition for all possible inputs. During development, you can attempt
such verification earlier than testing since it's performed modularly on a
per-subprogram basis. For example, in the code shown above, you can
formally verify Use_Find even before you write the body for subprogram
Find.
Advanced Contracts
Contracts for functional correctness are usually more complex than contracts for program integrity, so they more often require you to use the new forms of expressions introduced by the Ada 2012 standard. In particular, quantified expressions, which allow you to specify properties that must hold for all or for at least one element of a range, come in handy when specifying properties of arrays.
As contracts become more complex, you may find it useful to introduce new abstractions to improve the readability of your contracts. Expression functions are a good means to this end because you can retain their bodies in your package's specification.
Finally, some properties, especially those better described as invariants over data than as properties of subprograms, may be cumbersome to express as subprogram contracts. Type predicates, which must hold for every object of a given type, are usually a better match for this purpose. Here's an example.
package Show_Sort is
type Nat_Array is array (Positive range <>) of Natural;
function Is_Sorted (A : Nat_Array) return Boolean is
(for all I in A'Range =>
(if I < A'Last then A (I) <= A (I + 1)));
-- Returns True if A is sorted in increasing order.
subtype Sorted_Nat_Array is Nat_Array with
Dynamic_Predicate => Is_Sorted (Sorted_Nat_Array);
-- Elements of type Sorted_Nat_Array are all sorted.
Good_Array : Sorted_Nat_Array := (1, 2, 4, 8, 42);
end Show_Sort;
We can use the subtype Sorted_Nat_Array as the type of a variable that
must remain sorted throughout the program's execution. Specifying that an
array is sorted requires a rather complex expression involving quantifiers,
so we abstract away this property as an expression function to improve
readability. Is_Sorted's body remains in the package's specification
and allows users of the package to retain a precise knowledge of its
meaning when necessary. (You must use Nat_Array as the type of the
operand of Is_Sorted. If you use Sorted_Nat_Array, you'll get
infinite recursion at runtime when assertion checks are enabled since that
function is called to check all operands of type Sorted_Nat_Array.)
Ghost Code
As the properties you need to specify grow more complex, you may have
entities that are only needed because they are used in specifications
(contracts). You may find it important to ensure that these entities can't
affect the behavior of the program or that they're completely removed from
production code. This concept, having entities that are only used for
specifications, is usually called having ghost code and is supported in
SPARK by the Ghost aspect.
You can use Ghost aspects to annotate any entity including
variables, types, subprograms, and packages. If you mark an entity as
Ghost, GNATprove ensures it can't affect the program's
behavior. When the program is compiled with assertions enabled, ghost code
is executed like normal code so it can execute the contracts using it. You
can also instruct the compiler to not generate code for ghost entities.
Consider the procedure Do_Something below, which calls a complex
function on its input, X, and wants to check that the initial and
modified values of X are related in that complex way.
package Show_Ghost is
type T is record
A, B, C, D, E : Boolean;
end record;
function Formula (X : T) return Boolean is
((X.A and X.B) or (X.C and (X.D or X.E)));
function Is_Correct (X, Y : T) return Boolean is
(Formula (X) = Formula (Y));
procedure Do_Something (X : in out T);
end Show_Ghost;
package body Show_Ghost is
procedure Do_Some_Complex_Stuff (X : in out T) is
begin
X := T'(X.B, X.A, X.C, X.E, X.D);
end Do_Some_Complex_Stuff;
procedure Do_Something (X : in out T) is
X_Init : constant T := X with Ghost;
begin
Do_Some_Complex_Stuff (X);
pragma Assert (Is_Correct (X_Init, X));
-- It is OK to use X_Init inside an assertion.
end Do_Something;
end Show_Ghost;
Do_Something stores the initial value of X in a ghost constant,
X_Init. We reference it in an assertion to check that the computation
performed by the call to Do_Some_Complex_Stuff modified the value of
X in the expected manner.
However, X_Init can't be used in normal code, for example to restore
the initial value of X.
package Show_Ghost is
type T is record
A, B, C, D, E : Boolean;
end record;
function Formula (X : T) return Boolean is
((X.A and X.B) or (X.C and (X.D or X.E)));
function Is_Correct (X, Y : T) return Boolean is
(Formula (X) = Formula (Y));
procedure Do_Something (X : in out T);
end Show_Ghost;
package body Show_Ghost is
procedure Do_Some_Complex_Stuff (X : in out T) is
begin
X := T'(X.B, X.A, X.C, X.E, X.D);
end Do_Some_Complex_Stuff;
procedure Do_Something (X : in out T) is
X_Init : constant T := X with Ghost;
begin
Do_Some_Complex_Stuff (X);
pragma Assert (Is_Correct (X_Init, X));
X := X_Init; -- ERROR
end Do_Something;
end Show_Ghost;
with Show_Ghost; use Show_Ghost;
procedure Use_Ghost is
X : T := (True, True, False, False, True);
begin
Do_Something (X);
end Use_Ghost;
When compiling this example, the compiler flags the use of X_Init
as illegal, but more complex cases of interference between ghost and
normal code may sometimes only be detected when you run GNATprove.
Ghost Functions
Functions used only in specifications are a common occurrence when writing contracts for functional correctness. For example, expression functions used to simplify or factor out common patterns in contracts can usually be marked as ghost.
But ghost functions can do more than improve readability. In real-world programs, it's often the case that some information necessary for functional specification isn't accessible in the package's specification because of abstraction.
Making this information available to users of the packages is generally out of the question because that breaks the abstraction. Ghost functions come in handy in that case since they provide a way to give access to that information without making it available to normal client code.
Let's look at the following example.
package Stacks is
pragma Unevaluated_Use_Of_Old (Allow);
type Stack is private;
type Element is new Natural;
type Element_Array is array (Positive range <>) of Element;
Max : constant Natural := 100;
function Get_Model (S : Stack) return Element_Array with Ghost;
-- Returns an array as a model of a stack.
procedure Push (S : in out Stack; E : Element) with
Pre => Get_Model (S)'Length < Max,
Post => Get_Model (S) = Get_Model (S)'Old & E;
private
subtype Length_Type is Natural range 0 .. Max;
type Stack is record
Top : Length_Type := 0;
Content : Element_Array (1 .. Max) := (others => 0);
end record;
end Stacks;
Here, the type Stack is private. To specify the expected behavior of
the Push procedure, we need to go inside this abstraction and access
the values of the elements stored in S. For this, we introduce a
function Get_Model that returns an array as a representation of the
stack. However, we don't want code that uses the Stack package to use
Get_Model in normal code since this breaks our stack's abstraction.
Here's an example of trying to break that abstraction in the subprogram
Peek below.
package Stacks is
pragma Unevaluated_Use_Of_Old (Allow);
type Stack is private;
type Element is new Natural;
type Element_Array is array (Positive range <>) of Element;
Max : constant Natural := 100;
function Get_Model (S : Stack) return Element_Array with Ghost;
-- Returns an array as a model of a stack.
procedure Push (S : in out Stack; E : Element) with
Pre => Get_Model (S)'Length < Max,
Post => Get_Model (S) = Get_Model (S)'Old & E;
function Peek (S : Stack; I : Positive) return Element is
(Get_Model (S) (I)); -- ERROR
private
subtype Length_Type is Natural range 0 .. Max;
type Stack is record
Top : Length_Type := 0;
Content : Element_Array (1 .. Max) := (others => 0);
end record;
end Stacks;
We see that marking the function as Ghost achieves this goal: it
ensures that the subprogram Get_Model is never used in production code.
Global Ghost Variables
Though it happens less frequently, you may have specifications requiring you to store additional information in global variables that isn't needed in normal code. You should mark these global variables as ghost, allowing the compiler to remove them when assertions aren't enabled. You can use these variables for any purpose within the contracts that make up your specifications. A common scenario is writing specifications for subprograms that modify a complex or private global data structure: you can use these variables to provide a model for that structure that's updated by the ghost code as the program modifies the data structure itself.
You can also use ghost variables to store information about previous runs
of subprograms to specify temporal properties. In the following example, we
have two procedures, one that accesses a state A and the other that
accesses a state B. We use the ghost variable Last_Accessed_Is_A to
specify that B can't be accessed twice in a row without accessing A
in between.
package Call_Sequence is
type T is new Integer;
Last_Accessed_Is_A : Boolean := False with Ghost;
procedure Access_A with
Post => Last_Accessed_Is_A;
procedure Access_B with
Pre => Last_Accessed_Is_A,
Post => not Last_Accessed_Is_A;
-- B can only be accessed after A
end Call_Sequence;
package body Call_Sequence is
procedure Access_A is
begin
-- ...
Last_Accessed_Is_A := True;
end Access_A;
procedure Access_B is
begin
-- ...
Last_Accessed_Is_A := False;
end Access_B;
end Call_Sequence;
with Call_Sequence; use Call_Sequence;
procedure Main is
begin
Access_A;
Access_B;
Access_B; -- ERROR
end Main;
Let's look at another example. The specification of a subprogram's expected behavior is sometimes best expressed as a sequence of actions it must perform. You can use global ghost variables that store intermediate values of normal variables to write this sort of specification more easily.
For example, we specify the subprogram Do_Two_Things below in two
steps, using the ghost variable V_Interm to store the intermediate
value of V between those steps. We could also express this using an
existential quantification on the variable V_Interm, but it would be
impractical to iterate over all integers at runtime and this can't always
be written in SPARK because quantification is restricted to
for ... loop patterns.
Finally, supplying the value of the variable may help the prover verify the contracts.
package Action_Sequence is
type T is new Integer;
V_Interm : T with Ghost;
function First_Thing_Done (X, Y : T) return Boolean with Ghost;
function Second_Thing_Done (X, Y : T) return Boolean with Ghost;
procedure Do_Two_Things (V : in out T) with
Post => First_Thing_Done (V'Old, V_Interm)
and then Second_Thing_Done (V_Interm, V);
end Action_Sequence;
Note
For more details on ghost code, see the SPARK User's Guide.
Guide Proof
Since properties of interest for functional correctness are more complex than those involved in proofs of program integrity, we expect GNATprove to initially be unable to verify them even though they're valid. You'll find the techniques we discussed in Debugging Failed Proof Attempts to come in handy here. We now go beyond those techniques and focus on more ways of improving results in the cases where the property is valid but GNATprove can't prove it in a reasonable amount of time.
In those cases, you may want to try and guide GNATprove to either complete the proof or strip it down to a small number of easily-reviewable assumptions. For this purpose, you can add assertions to break complex proofs into smaller steps.
pragma Assert (Assertion_Checked_By_The_Tool);
-- info: assertion proved
pragma Assert (Assumption_Validated_By_Other_Means);
-- medium: assertion might fail
pragma Assume (Assumption_Validated_By_Other_Means);
-- The tool does not attempt to check this expression.
-- It is recorded as an assumption.
One such intermediate step you may find useful is to try to prove a theoretically-equivalent version of the desired property, but one where you've simplified things for the prover, such as by splitting up different cases or inlining the definitions of functions.
Some intermediate assertions may not be proved by GNATprove either because
it's missing some information or because the amount of information
available is confusing. You can verify these remaining assertions by other
means such as testing (since they're executable) or by review. You can then
choose to instruct GNATprove to ignore them, either by turning them into
assumptions, as in our example, or by using a pragma Annotate. In
both cases, the compiler generates code to check these assumptions at
runtime when you enable assertions.
Local Ghost Variables
You can use ghost code to enhance what you can express inside intermediate
assertions in the same way we did above to enhance our contracts in
specifications. In particular, you'll commonly have local variables or
constants whose only purpose is to be used in assertions. You'll mostly
use these ghost variables to store previous values of variables or
expressions you want to refer to in assertions. They're especially useful
to refer to initial values of parameters and expressions since the
'Old attribute is only allowed in postconditions.
In the example below, we want to help GNATprove verify the postcondition of
P. We do this by introducing a local ghost constant, X_Init, to
represent this value and writing an assertion in both branches of an
if statement that repeats the postcondition, but using X_Init.
package Show_Local_Ghost is
type T is new Natural;
function F (X, Y : T) return Boolean is (X > Y) with Ghost;
function Condition (X : T) return Boolean is (X mod 2 = 0);
procedure P (X : in out T) with
Pre => X < 1_000_000,
Post => F (X, X'Old);
end Show_Local_Ghost;
package body Show_Local_Ghost is
procedure P (X : in out T) is
X_Init : constant T := X with Ghost;
begin
if Condition (X) then
X := X + 1;
pragma Assert (F (X, X_Init));
else
X := X * 2;
pragma Assert (F (X, X_Init));
end if;
end P;
end Show_Local_Ghost;
You can also use local ghost variables for more complex purposes such as
building a data structure that serves as witness for a complex property of
a subprogram. In our example, we want to prove that the Sort procedure
doesn't create new elements, that is, that all the elements present in
A after the sort were in A before the sort. This property isn't
enough to ensure that a call to Sort produces a value for A that's
a permutation of its value before the call (or that the values are indeed
sorted). However, it's already complex for a prover to verify because it
involves a nesting of quantifiers. To help GNATprove, you may find it
useful to store, for each index I, an index J that has the expected
property.
procedure Sort (A : in out Nat_Array) with
Post => (for all I in A'Range =>
(for some J in A'Range => A (I) = A'Old (J)))
is
Permutation : Index_Array := (1 => 1, 2 => 2, ...) with Ghost;
begin
...
end Sort;
Ghost Procedures
Ghost procedures can't affect the value of normal variables, so they're mostly used to perform operations on ghost variables or to group together a set of intermediate assertions.
Abstracting away the treatment of assertions and ghost variables inside a ghost procedure has several advantages. First, you're allowed to use these variables in any way you choose in code inside ghost procedures. This isn't the case outside ghost procedures, where the only ghost statements allowed are assignments to ghost variables and calls to ghost procedures.
As an example, the for loop contained in Increase_A couldn't
appear by itself in normal code.
package Show_Ghost_Proc is
type Nat_Array is array (Integer range <>) of Natural;
A : Nat_Array (1 .. 100) with Ghost;
procedure Increase_A with
Ghost,
Pre => (for all I in A'Range => A (I) < Natural'Last);
end Show_Ghost_Proc;
package body Show_Ghost_Proc is
procedure Increase_A is
begin
for I in A'Range loop
A (I) := A (I) + 1;
end loop;
end Increase_A;
end Show_Ghost_Proc;
Using the abstraction also improves readability by hiding complex code that isn't part of the functional behavior of the subprogram. Finally, it can help GNATprove by abstracting away assertions that would otherwise make its job more complex.
In the example below, calling Prove_P with X as an operand only
adds P (X) to the proof context instead of the larger set of assertions
required to verify it. In addition, the proof of P need only be done
once and may be made easier not having any unnecessary information present
in its context while verifying it. Also, if GNATprove can't fully verify
Prove_P, you can review the remaining assumptions more easily since
they're in a smaller context.
procedure Prove_P (X : T) with Ghost,
Global => null,
Post => P (X);
Handling of Loops
When the program involves a loop, you're almost always required to provide additional annotations to allow GNATprove to complete a proof because the verification techniques used by GNATprove don't handle cycles in a subprogram's control flow. Instead, loops are flattened by dividing them into several acyclic parts.
As an example, let's look at a simple loop with an exit condition.
Stmt1;
loop
Stmt2;
exit when Cond;
Stmt3;
end loop;
Stmt4;
As shown below, the control flow is divided into three parts.
The first, shown in yellow, starts earlier in the subprogram and enters the loop statement. The loop itself is divided into two parts. Red represents a complete execution of the loop's body: an execution where the exit condition isn't satisfied. Blue represents the last execution of the loop, which includes some of the subprogram following it. For that path, the exit condition is assumed to hold. The red and blue parts are always executed after the yellow one.
GNATprove analyzes these parts independently since it doesn't have a way to track how variables may have been updated by an iteration of the loop. It forgets everything it knows about those variables from one part when entering another part. However, values of constants and variables that aren't modified in the loop are not an issue.
In other words, handling loops in that way makes GNATprove imprecise when verifying a subprogram involving a loop: it can't verify a property that relies on values of variables modified inside the loop. It won't forget any information it had on the value of constants or unmodified variables, but it nevertheless won't be able to deduce new information about them from the loop.
For example, consider the function Find which iterates over the array
A and searches for an element where E is stored in A.
package Show_Find is
type Nat_Array is array (Positive range <>) of Natural;
function Find (A : Nat_Array; E : Natural) return Natural;
end Show_Find;
package body Show_Find is
function Find (A : Nat_Array; E : Natural) return Natural is
begin
for I in A'Range loop
pragma Assert (for all J in A'First .. I - 1 => A (J) /= E);
-- assertion is not proved
if A (I) = E then
return I;
end if;
pragma Assert (A (I) /= E);
-- assertion is proved
end loop;
return 0;
end Find;
end Show_Find;
At the end of each loop iteration, GNATprove knows that the value stored at
index I in A must not be E. (If it were, the loop wouldn't
have reached the end of the interation.) This proves the second assertion. But
it's unable to aggregate this information over multiple loop iterations to
deduce that it's true for all the indexes smaller than I, so it can't
prove the first assertion.
Loop Invariants
To overcome these limitations, you can provide additional information to GNATprove in the form of a loop invariant. In SPARK, a loop invariant is a Boolean expression which holds true at every iteration of the loop. Like other assertions, you can have it checked at runtime by compiling the program with assertions enabled.
The major difference between loop invariants and other assertions is the way it's treated for proofs. GNATprove performs the proof of a loop invariant in two steps: first, it checks that it holds for the first iteration of the loop and then it checks that it holds in an arbitrary iteration assuming it held in the previous iteration. This is called proof by induction.
As an example, let's add a loop invariant to the Find function stating
that the first element of A is not E.
package Show_Find is
type Nat_Array is array (Positive range <>) of Natural;
function Find (A : Nat_Array; E : Natural) return Natural;
end Show_Find;
package body Show_Find is
function Find (A : Nat_Array; E : Natural) return Natural is
begin
for I in A'Range loop
pragma Loop_Invariant (A (A'First) /= E);
-- loop invariant not proved in first iteration
-- but preservation of loop invariant is proved
if A (I) = E then
return I;
end if;
end loop;
return 0;
end Find;
end Show_Find;
To verify this invariant, GNATprove generates two checks. The first checks
that the assertion holds in the first iteration of the loop. This isn't
verified by GNATprove. And indeed there's no reason to expect the first
element of A to always be different from E in this iteration.
However, the second check is proved: it's easy to deduce that if the first
element of A was not E in a given iteration it's still not E in
the next. However, if we move the invariant to the end of the loop, then it
is successfully verified by GNATprove.
Not only do loop invariants allow you to verify complex properties of loops, but GNATprove also uses them to verify other properties, such as the absence of runtime errors over both the loop's body and the statements following the loop. More precisely, when verifying a runtime check or other assertion there, GNATprove assumes that the last occurrence of the loop invariant preceding the check or assertion is true.
Let's look at a version of Find where we use a loop invariant instead
of an assertion to state that none of the array elements seen so far are
equal to E.
package Show_Find is
type Nat_Array is array (Positive range <>) of Natural;
function Find (A : Nat_Array; E : Natural) return Natural;
end Show_Find;
package body Show_Find is
function Find (A : Nat_Array; E : Natural) return Natural is
begin
for I in A'Range loop
pragma Loop_Invariant
(for all J in A'First .. I - 1 => A (J) /= E);
if A (I) = E then
return I;
end if;
end loop;
pragma Assert (for all I in A'Range => A (I) /= E);
return 0;
end Find;
end Show_Find;
This version is fully verified by GNATprove! This time, it proves that the
loop invariant holds in every iteration of the loop (separately proving
this property for the first iteration and then for the following
iterations). It also proves that none of the elements of A are equal to
E after the loop exits by assuming that the loop invariant holds in the
last iteration of the loop.
Note
For more details on loop invariants, see the SPARK User's Guide.
Finding a good loop invariant can turn out to be quite a challenge. To make this task easier, let's review the four good properties of a good loop invariant:
Property |
Description |
|---|---|
INIT |
It should be provable in the first iteration of the loop. |
INSIDE |
It should allow proving the absence of run-time errors and local assertions inside the loop. |
AFTER |
It should allow proving absence of run-time errors, local assertions, and the subprogram postcondition after the loop. |
PRESERVE |
It should be provable after the first iteration of the loop. |
Let's look at each of these in turn. First, the loop invariant should be provable in the first iteration of the loop (INIT). If your invariant fails to achieve this property, you can debug the loop invariant's initialization like any failing proof attempt using strategies for Debugging Failed Proof Attempts.
Second, the loop invariant should be precise enough to allow GNATprove to prove absence of runtime errors in both statements from the loop's body (INSIDE) and those following the loop (AFTER). To do this, you should remember that all information concerning a variable modified in the loop that's not included in the invariant is forgotten by GNATprove. In particular, you should take care to include in your invariant what's usually called the loop's frame condition, which lists properties of variables that are true throughout the execution of the loop even though those variables are modified by the loop.
Finally, the loop invariant should be precise enough to prove that it's preserved through successive iterations of the loop (PRESERVE). This is generally the trickiest part. To understand why GNATprove hasn't been able to verify the preservation of a loop invariant you provided, you may find it useful to repeat it as local assertions throughout the loop's body to determine at which point it can no longer be proved.
As an example, let's look at a loop that iterates through an array A
and applies a function F to each of its elements.
package Show_Map is
type Nat_Array is array (Positive range <>) of Natural;
function F (V : Natural) return Natural is
(if V /= Natural'Last then V + 1 else V);
procedure Map (A : in out Nat_Array);
end Show_Map;
package body Show_Map is
procedure Map (A : in out Nat_Array) is
A_I : constant Nat_Array := A with Ghost;
begin
for K in A'Range loop
A (K) := F (A (K));
pragma Loop_Invariant
(for all J in A'First .. K => A (J) = F (A'Loop_Entry (J)));
end loop;
pragma Assert (for all K in A'Range => A (K) = F (A_I (K)));
end Map;
end Show_Map;
After the loop, each element of A should be the result of applying
F to its previous value. We want to prove this. To specify this
property, we copy the value of A before the loop into a ghost variable,
A_I. Our loop invariant states that the element at each index less than
K has been modified in the expected way. We use the Loop_Entry
attribute to refer to the value of A on entry of the loop instead of
using A_I.
Does our loop invariant have the four properties of a good loop-invariant?
When launching GNATprove, we see that INIT is fulfilled: the
invariant's initialization is proved. So are INSIDE and AFTER: no
potential runtime errors are reported and the assertion following the loop
is successfully verified.
The situation is slightly more complex for the PRESERVE
property. GNATprove manages to prove that the invariant holds after the
first iteration thanks to the automatic generation of frame conditions. It
was able to do this because it completes the provided loop invariant with
the following frame condition stating what part of the array hasn't been
modified so far:
pragma Loop_Invariant
(for all J in K .. A'Last => A (J) = (if J > K then A'Loop_Entry (J)));
GNATprove then uses both our and the internally-generated loop invariants
to prove PRESERVE. However, in more complex cases, the heuristics used
by GNATprove to generate the frame condition may not be sufficient and
you'll have to provide one as a loop invariant. For example, consider a
version of Map where the result of applying F to an element at
index K is stored at index K-1:
package Show_Map is
type Nat_Array is array (Positive range <>) of Natural;
function F (V : Natural) return Natural is
(if V /= Natural'Last then V + 1 else V);
procedure Map (A : in out Nat_Array);
end Show_Map;
package body Show_Map is
procedure Map (A : in out Nat_Array) is
A_I : constant Nat_Array := A with Ghost;
begin
for K in A'Range loop
if K /= A'First then
A (K - 1) := F (A (K));
end if;
pragma Loop_Invariant
(for all J in A'First .. K =>
(if J /= A'First then A (J - 1) = F (A'Loop_Entry (J))));
-- pragma Loop_Invariant
-- (for all J in K .. A'Last => A (J) = A'Loop_Entry (J));
end loop;
pragma Assert (for all K in A'Range =>
(if K /= A'First then A (K - 1) = F (A_I (K))));
end Map;
end Show_Map;
You need to uncomment the second loop invariant containing the frame condition in order to prove the assertion after the loop.
Note
For more details on how to write a loop invariant, see the SPARK User's Guide.
Code Examples / Pitfalls
This section contains some code examples and pitfalls.
Example #1
We implement a ring buffer inside an array Content, where the contents
of a ring buffer of length Length are obtained by starting at index
First and possibly wrapping around the end of the buffer. We use a
ghost function Get_Model to return the contents of the ring buffer for
use in contracts.
package Ring_Buffer is
Max_Size : constant := 100;
type Nat_Array is array (Positive range <>) of Natural;
function Get_Model return Nat_Array with Ghost;
procedure Push_Last (E : Natural) with
Pre => Get_Model'Length < Max_Size,
Post => Get_Model'Length = Get_Model'Old'Length + 1;
end Ring_Buffer;
package body Ring_Buffer is
subtype Length_Range is Natural range 0 .. Max_Size;
subtype Index_Range is Natural range 1 .. Max_Size;
Content : Nat_Array (1 .. Max_Size) := (others => 0);
First : Index_Range := 1;
Length : Length_Range := 0;
function Get_Model return Nat_Array with
Refined_Post => Get_Model'Result'Length = Length
is
Size : constant Length_Range := Length;
Result : Nat_Array (1 .. Size) := (others => 0);
begin
if First + Length - 1 <= Max_Size then
Result := Content (First .. First + Length - 1);
else
declare
Len : constant Length_Range := Max_Size - First + 1;
begin
Result (1 .. Len) := Content (First .. Max_Size);
Result (Len + 1 .. Length) := Content (1 .. Length - Len);
end;
end if;
return Result;
end Get_Model;
procedure Push_Last (E : Natural) is
begin
if First + Length <= Max_Size then
Content (First + Length) := E;
else
Content (Length - Max_Size + First) := E;
end if;
Length := Length + 1;
end Push_Last;
end Ring_Buffer;
This is correct: Get_Model is used only in contracts. Calls to
Get_Model make copies of the buffer's contents, which isn't efficient,
but is fine because Get_Model is only used for verification, not in
production code. We enforce this by making it a ghost function. We'll
produce the final production code with appropriate compiler switches (i.e.,
not using -gnata) that ensure assertions are ignored.
Example #2
Instead of using a ghost function, Get_Model, to retrieve the contents
of the ring buffer, we're now using a global ghost variable, Model.
package Ring_Buffer is
Max_Size : constant := 100;
subtype Length_Range is Natural range 0 .. Max_Size;
subtype Index_Range is Natural range 1 .. Max_Size;
type Nat_Array is array (Positive range <>) of Natural;
type Model_Type (Length : Length_Range := 0) is record
Content : Nat_Array (1 .. Length);
end record
with Ghost;
Model : Model_Type with Ghost;
function Valid_Model return Boolean;
procedure Push_Last (E : Natural) with
Pre => Valid_Model
and then Model.Length < Max_Size,
Post => Model.Length = Model.Length'Old + 1;
end Ring_Buffer;
package body Ring_Buffer is
Content : Nat_Array (1 .. Max_Size) := (others => 0);
First : Index_Range := 1;
Length : Length_Range := 0;
function Valid_Model return Boolean is
(Model.Content'Length = Length);
procedure Push_Last (E : Natural) is
begin
if First + Length <= Max_Size then
Content (First + Length) := E;
else
Content (Length - Max_Size + First) := E;
end if;
Length := Length + 1;
end Push_Last;
end Ring_Buffer;
This example isn't correct. Model, which is a ghost variable, must not
influence the return value of the normal function Valid_Model. Since
Valid_Model is only used in specifications, we should have marked it as
Ghost. Another problem is that Model needs to be updated inside
Push_Last to reflect the changes to the ring buffer.
Example #3
Let's mark Valid_Model as Ghost and update Model inside
Push_Last.
package Ring_Buffer is
Max_Size : constant := 100;
subtype Length_Range is Natural range 0 .. Max_Size;
subtype Index_Range is Natural range 1 .. Max_Size;
type Nat_Array is array (Positive range <>) of Natural;
type Model_Type (Length : Length_Range := 0) is record
Content : Nat_Array (1 .. Length);
end record
with Ghost;
Model : Model_Type with Ghost;
function Valid_Model return Boolean with Ghost;
procedure Push_Last (E : Natural) with
Pre => Valid_Model
and then Model.Length < Max_Size,
Post => Model.Length = Model.Length'Old + 1;
end Ring_Buffer;
package body Ring_Buffer is
Content : Nat_Array (1 .. Max_Size) := (others => 0);
First : Index_Range := 1;
Length : Length_Range := 0;
function Valid_Model return Boolean is
(Model.Content'Length = Length);
procedure Push_Last (E : Natural) is
begin
if First + Length <= Max_Size then
Content (First + Length) := E;
else
Content (Length - Max_Size + First) := E;
end if;
Length := Length + 1;
Model := (Length => Model.Length + 1,
Content => Model.Content & E);
end Push_Last;
end Ring_Buffer;
This example is correct. The ghost variable Model can be referenced
both from the body of the ghost function Valid_Model and the non-ghost
procedure Push_Last as long as it's only used in ghost statements.
Example #4
We're now modifying Push_Last to share the computation of the new
length between the operational and ghost code.
package Ring_Buffer is
Max_Size : constant := 100;
subtype Length_Range is Natural range 0 .. Max_Size;
subtype Index_Range is Natural range 1 .. Max_Size;
type Nat_Array is array (Positive range <>) of Natural;
type Model_Type (Length : Length_Range := 0) is record
Content : Nat_Array (1 .. Length);
end record
with Ghost;
Model : Model_Type with Ghost;
function Valid_Model return Boolean with Ghost;
procedure Push_Last (E : Natural) with
Pre => Valid_Model
and then Model.Length < Max_Size,
Post => Model.Length = Model.Length'Old + 1;
end Ring_Buffer;
package body Ring_Buffer is
Content : Nat_Array (1 .. Max_Size) := (others => 0);
First : Index_Range := 1;
Length : Length_Range := 0;
function Valid_Model return Boolean is
(Model.Content'Length = Length);
procedure Push_Last (E : Natural) is
New_Length : constant Length_Range := Model.Length + 1;
begin
if First + Length <= Max_Size then
Content (First + Length) := E;
else
Content (Length - Max_Size + First) := E;
end if;
Length := New_Length;
Model := (Length => New_Length,
Content => Model.Content & E);
end Push_Last;
end Ring_Buffer;
This example isn't correct. We didn't mark local constant New_Length as
Ghost, so it can't be computed from the value of ghost variable
Model. If we made New_Length a ghost constant, the compiler would
report the problem on the assignment from New_Length to Length. The
correct solution here is to compute New_Length from the value of the
non-ghost variable Length.
Example #5
Let's move the code updating Model inside a local ghost procedure,
Update_Model, but still using a local variable, New_Length, to
compute the length.
package Ring_Buffer is
Max_Size : constant := 100;
subtype Length_Range is Natural range 0 .. Max_Size;
subtype Index_Range is Natural range 1 .. Max_Size;
type Nat_Array is array (Positive range <>) of Natural;
type Model_Type (Length : Length_Range := 0) is record
Content : Nat_Array (1 .. Length);
end record
with Ghost;
Model : Model_Type with Ghost;
function Valid_Model return Boolean with Ghost;
procedure Push_Last (E : Natural) with
Pre => Valid_Model
and then Model.Length < Max_Size,
Post => Model.Length = Model.Length'Old + 1;
end Ring_Buffer;
package body Ring_Buffer is
Content : Nat_Array (1 .. Max_Size) := (others => 0);
First : Index_Range := 1;
Length : Length_Range := 0;
function Valid_Model return Boolean is
(Model.Content'Length = Length);
procedure Push_Last (E : Natural) is
procedure Update_Model with Ghost is
New_Length : constant Length_Range := Model.Length + 1;
begin
Model := (Length => New_Length,
Content => Model.Content & E);
end Update_Model;
begin
if First + Length <= Max_Size then
Content (First + Length) := E;
else
Content (Length - Max_Size + First) := E;
end if;
Length := Length + 1;
Update_Model;
end Push_Last;
end Ring_Buffer;
Everything's fine here. Model is only accessed inside Update_Model,
itself a ghost procedure, so it's fine to declare local variable
New_Length without the Ghost aspect: everything inside a ghost
procedure body is ghost. Moreover, we don't need to add any contract to
Update_Model: it's inlined by GNATprove because it's a local procedure
without a contract.
Example #6
The function Max_Array takes two arrays of the same length (but not
necessarily with the same bounds) as arguments and returns an array with
each entry being the maximum values of both arguments at that index.
package Array_Util is
type Nat_Array is array (Positive range <>) of Natural;
function Max_Array (A, B : Nat_Array) return Nat_Array with
Pre => A'Length = B'Length;
end Array_Util;
package body Array_Util is
function Max_Array (A, B : Nat_Array) return Nat_Array is
R : Nat_Array (A'Range);
J : Integer := B'First;
begin
for I in A'Range loop
if A (I) > B (J) then
R (I) := A (I);
else
R (I) := B (J);
end if;
J := J + 1;
end loop;
return R;
end Max_Array;
end Array_Util;
This program is correct, but GNATprove can't prove that J is always in
the index range of B (the unproved index check) or even that it's
always within the bounds of its type (the unproved overflow check). Indeed,
when checking the body of the loop, GNATprove forgets everything about the
current value of J because it's been modified by previous loop
iterations. To get more precise results, we need to provide a loop
invariant.
Example #7
Let's add a loop invariant that states that J stays in the index range
of B and let's protect the increment to J by checking that it's not
already the maximal integer value.
package Array_Util is
type Nat_Array is array (Positive range <>) of Natural;
function Max_Array (A, B : Nat_Array) return Nat_Array with
Pre => A'Length = B'Length;
end Array_Util;
package body Array_Util is
function Max_Array (A, B : Nat_Array) return Nat_Array is
R : Nat_Array (A'Range);
J : Integer := B'First;
begin
for I in A'Range loop
pragma Loop_Invariant (J in B'Range);
if A (I) > B (J) then
R (I) := A (I);
else
R (I) := B (J);
end if;
if J < Integer'Last then
J := J + 1;
end if;
end loop;
return R;
end Max_Array;
end Array_Util;
The loop invariant now allows verifying that no runtime error can occur in
the loop's body (property INSIDE seen in section Loop Invariants).
Unfortunately, GNATprove fails to verify that the invariant
stays valid after the first iteration of the loop (property
PRESERVE). Indeed, knowing that J is in B'Range in a given
iteration isn't enough to prove it'll remain so in the next iteration. We
need a more precise invariant, linking J to the value of the loop index
I, like J = I - A'First + B'First.
Example #8
We now consider a version of Max_Array which takes arguments that have
the same bounds. We want to prove that Max_Array returns an array of
the maximum values of both its arguments at each index.
package Array_Util is
type Nat_Array is array (Positive range <>) of Natural;
function Max_Array (A, B : Nat_Array) return Nat_Array with
Pre => A'First = B'First and A'Last = B'Last,
Post => (for all K in A'Range =>
Max_Array'Result (K) = Natural'Max (A (K), B (K)));
end Array_Util;
package body Array_Util is
function Max_Array (A, B : Nat_Array) return Nat_Array is
R : Nat_Array (A'Range) := (others => 0);
begin
for I in A'Range loop
pragma Loop_Invariant (for all K in A'First .. I =>
R (K) = Natural'Max (A (K), B (K)));
if A (I) > B (I) then
R (I) := A (I);
else
R (I) := B (I);
end if;
end loop;
return R;
end Max_Array;
end Array_Util;
with Array_Util; use Array_Util;
procedure Main is
A : Nat_Array := (1, 1, 2);
B : Nat_Array := (2, 1, 0);
R : Nat_Array (1 .. 3);
begin
R := Max_Array (A, B);
end Main;
Here, GNATprove doesn't manage to prove the loop invariant even for the
first loop iteration (property INIT seen in section Loop Invariants).
In fact, the loop invariant is incorrect, as you can see by
executing the function Max_Array with assertions enabled: at each loop
iteration, R contains the maximum of A and B only until
I - 1 because the I'th index wasn't yet handled.
Example #9
We now consider a procedural version of Max_Array which updates its
first argument instead of returning a new array. We want to prove that
Max_Array sets the maximum values of both its arguments into each index
in its first argument.
package Array_Util is
type Nat_Array is array (Positive range <>) of Natural;
procedure Max_Array (A : in out Nat_Array; B : Nat_Array) with
Pre => A'First = B'First and A'Last = B'Last,
Post => (for all K in A'Range =>
A (K) = Natural'Max (A'Old (K), B (K)));
end Array_Util;
package body Array_Util is
procedure Max_Array (A : in out Nat_Array; B : Nat_Array) is
begin
for I in A'Range loop
pragma Loop_Invariant
(for all K in A'First .. I - 1 =>
A (K) = Natural'Max (A'Loop_Entry (K), B (K)));
pragma Loop_Invariant
(for all K in I .. A'Last => A (K) = A'Loop_Entry (K));
if A (I) <= B (I) then
A (I) := B (I);
end if;
end loop;
end Max_Array;
end Array_Util;
Everything is proved. The first loop invariant states that the values of
A before the loop index contains the maximum values of the arguments of
Max_Array (referring to the input value of A with
A'Loop_Entry). The second loop invariant states that the values of
A beyond and including the loop index are the same as they were on
entry. This is the frame condition of the loop.
Example #10
Let's remove the frame condition from the previous example.
package Array_Util is
type Nat_Array is array (Positive range <>) of Natural;
procedure Max_Array (A : in out Nat_Array; B : Nat_Array) with
Pre => A'First = B'First and A'Last = B'Last,
Post => (for all K in A'Range =>
A (K) = Natural'Max (A'Old (K), B (K)));
end Array_Util;
package body Array_Util is
procedure Max_Array (A : in out Nat_Array; B : Nat_Array) is
begin
for I in A'Range loop
pragma Loop_Invariant
(for all K in A'First .. I - 1 =>
A (K) = Natural'Max (A'Loop_Entry (K), B (K)));
if A (I) <= B (I) then
A (I) := B (I);
end if;
end loop;
end Max_Array;
end Array_Util;
Everything is still proved. GNATprove internally generates the frame
condition for the loop, so it's sufficient here to state that A before
the loop index contains the maximum values of the arguments of
Max_Array.