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.

with Ada.Text_IO; use Ada.Text_IO; 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;

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 doesn'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.

../../../_images/05_loop.png

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.

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.

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) := (others => 0); 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) := (others => 0); 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.