Formal Verification with GNATprove

The GNATprove tool is packaged as an executable called gnatprove. Like other tools in GNAT Pro Toolsuite, GNATprove is based on the structure of GNAT projects, defined in .gpr files.

How to Run GNATprove

Running GNATprove from the Command Line

GNATprove can be run from the command line as follows:

gnatprove -P <project-file.gpr>

In the appendix, section Command-line Options, you can find an exhaustive list of switches; here we only give an overview over the most common uses. Note that GNATprove cannot be run without a project file.

When given a list of files, GNATprove will consider them as entry points of the program and analyze these units and all units on which they depend. With option -u, the dependencies are not considered, only the given files themselves are analyzed. With option -U, all files of all projects are proved.

GNATprove consists of two distinct analyses, flow analysis and proof. Flow analysis checks the correctness of Globals and Depends aspects, and verifies the initialization of variables. Proof verifies the absence of runtime errors and the correctness of assertions such as Pre and Post aspects. Using the switch --mode=<mode>, whose possible values are prove, flow and all, you can choose to perform only one or both of these analyses. Today, flow analysis is experimental, so prove is the default. In the future, all will be the default.

Using the option --limit-line= one can limit proofs to a particular file and line of an Ada file. For example, if you want to prove only the file 12 of file example.adb, you can add the option --limit-line=example.adb:12 to the call to GNATprove. Using the option --limit-subp= one can limit proofs to a subprogram declared in a particular file at a particular line.

A number of options exist to influence the behavior for proof. Internally, the prover Alt-Ergo is called repeatedly for each check or assertion. Using the option --timeout, one can change the maximal time that is allocated to prove each check or assertion (default: 1s). Using the option --steps (default: not used), one can set the maximum number of reasoning steps that Alt-Ergo is allowed to perform before giving up. The steps option should be used when predictable results are required, because the results with a timeout may differ depending on the computing power or current load of the machine. The option -j activates parallel compilation and parallel proofs.

The way checks are passed to Alt-Ergo can also be influenced using the option --proof. By default, Alt-Ergo is invoked a single time for each check or assertion (mode no_split). This can be changed using mode path_wp to invoke Alt-Ergo for each path that leads to the check. This option usually takes much longer, because Alt-Ergo is invoked much more often, but may give better proof results. Using mode all-split, in addition, conjunctions (such as and and and then) in assertions are split and passed seperately to Alt-Ergo. Finally, in mode then-split, invoking Alt-Ergo a single time on the entire check is tried, and only if the check is not proved, the other techniques (splitting conjunctions and trying each path separately) are tried.

By default, GNATprove avoids reanalyzing unchanged files, on a per-unit basis. This mechanism can be disabled with the option -f.

Implementation-Defined Behavior

A SPARK 2014 program is guaranteed to be unambiguous, so that formal verification of properties is possible. However, some behaviors may depend on the compiler used. By default, GNATprove adopts the same choices as the GNAT compiler. GNATprove also supports other compilers by providing special switches:

• -gnateT for specifying the target configuration
• --pedantic for warning about possible implementation-defined behavior

With option --pedantic, some compiler choices are forced to a worst-case interpretation of the Ada standard. For example, ranges for integer base types are reduced to the minimum guaranteed, not to the matching machine integer type as done in practice on all compilers.

Target Parametrization

Target parametrization consists in passing to GNATprove a file which defines the parameters for the target on which the program will be run. These include the size and alignment of standard integer types, endianness, the kinds of floating-point numbers, etc. The format of this file should match the format of the file generated by calling GNAT Pro with switch -gnatet.

Target parametrization can be used:

• to specify a target different than the host on which GNATprove is run, when cross-compilation is used. If GNAT Pro is the cross compiler, the configuration file can be generated by calling it with the switch -gnatet=?. Otherwise, the target file should be generated manually.
• to specify the parameters for a different compiler than GNAT Pro, even when the host and target are the same. In that case, the target file should be generated manually.

Parenthesized Arithmetic Operations

In Ada, non-parenthesized arithmetic operations could be re-ordered by the compiler, which may result in a failing computation (due to overflow checking) becoming a successful one, and vice-versa. By default, GNATprove evaluates allexpressions left-to-right, like GNAT. When the switch --pedantic is used, a warning is emitted for every operation that could be re-ordered:

• any operand of a binary adding operation (+,-) that is itself a binary adding operation;
• any operand of a binary multiplying operation (*,/,mod,rem) that is itself a binary multiplying operation.

Compiler Permissions

Ada standard defines various ways in which a compiler is allowed to compute a correct result for a computation instead of raising a run-time error. By default, GNATprove adopts the choices made by GNAT on the platform. When the switch --pedantic is used, GNATprove interprets all computations with the strictest meaning guaranteed by Ada Reference Manual.

For example, the bounds of base types for user-defined types, which define which computations overflow, may vary depending on the compiler and host/target architectures. With option --pedantic, all bounds should be set to their minimum range guaranteed by the Ada standard (worst case). For example, the following type should have a base type ranging from -10 to 10 (standard requires a symmetric range with a possible extra negative value):

type T is 1 .. 10;

This other type should have a base type ranging from -10 to 9:

type T is -10 .. 1;

Running GNATprove from GPS

GNATprove can be run from GPS. There is a menu Prove with the following entries:

Submenu	Action
Prove All	This runs GNATprove on all files in the project.
Prove Root Project	This runs GNATprove on the entire project.
Prove File	This runs GNATprove on the current unit.
Clean Proofs	This removes all files generated by GNATprove.
Remove Editor Highlighting	This removes highlighting generated by using GNATprove.

Note

The changes made by users in the panels raised by these submenus are persistent from one session to the other. Be sure to check that the selected checkboxes and additional switches that were previously added are still appropriate.

When editing an Ada file, GNATprove can also be run from the context menu, which can be obtained by a right click:

Submenu	Action
Prove File	This runs GNATprove on the current unit.
Prove Line	This runs proofs on the checks of the current line of the current file.
Prove Subprogram	This runs proofs on the checks of the current subprogram.

Note

If you use the SPARK-HiLite GPL 2013 release, a fourth submenu Show Path is present in the contextual menu, that displays a path in the editor corresponding to the current error message. This highlighting can be removed by selecting Prove --> Remove Editor Highlighting.

GNATprove project switches can be edited from the panel GNATprove (in Project --> Edit Project Properties --> Switches).

In some proof modes (--proof=then_split or --proof=path_wp), GNATprove attempts to prove checks separately for the possible paths leading to a check. If the proof fails on a specific path, the user can display this path in GPS by clicking on the icon to the left of the failed proof message, or to the left of the corresponding line in the editor. The path is hidden again when re-clicking on the same icon.

Note

If you use the SPARK-HiLite GPL 2013 release, the way to display a path in GPS is slightly different. Instead of clicking on an icon, you need to right-click on the error message in the Location View, and select Prove::Show Path in the contextual menu that is raised.

We recommend that you enable the option Draw current line as a thin line (in Edit --> Preferences --> Editor --> Fonts & Colors) so that GPS does not hide the status of the checks on the current line (all proved in green / otherwise in red). This is the default on recent versions of GPS.

How to View GNATprove Output

In mode check, GNATprove prints on the standard output error messages for SPARK 2014 subset violations, and warning messages for unimplemented features, on all the code for which SPARK_Mode is On.

In mode prove and report fail, GNATprove prints on the standard output error messages for unproved VCs.

In mode prove and report all or statistics, GNATprove prints on the standard output error messages for unproved VCs, and information messages for proved VCs.

In mode flow, GNATprove prints on the standard output error messages and warnings for incorrect Globals and depends contracts, unitialized error messages, and suspicious situations such as unused assignments, missing return statements and so on.

In mode all, GNATprove behaves just as if both modes prove and flow were activated.

GNATprove always generates Project Statistics in file gnatprove.out.

For each unit <name>, GNATprove generates a Summary File <name>.alfa in the sub-directory gnatprove of the corresponding object directory.

Project Statistics

Based on the automatic detection of which subprograms are in SPARK 2014, GNATprove generates global project statistics in file gnatprove.out. The statistics describe:

• what percentage and number of subprograms are in SPARK 2014
• what percentage and number of SPARK 2014 subprograms are not yet supported
• what are the main reasons for subprograms not to be in SPARK 2014
• what are the main reasons for subprograms not to be yet supported in SPARK 2014
• units with the largest number of subprograms in SPARK 2014
• units with the largest number of subprograms not in SPARK 2014

Summary File

The information of which subprogram specs and bodies are in SPARK 2014 is stored in a file with extension .alfa for review by the user, and to produce global Project Statistics. GNATprove outputs the reasons for which a subprogram is not in SPARK 2014 (using parentheses):

• access: access types and dereferences;
• assembly language: assembly language;
• deallocation: unchecked deallocation;
• dynamic allocation: dynamic allocation;
• exception: raising and catching exceptions;
• forward reference: forward reference to an entity;
• goto: use of goto;
• indirect call: indirect call;
• tasking: tasking;
• unchecked conversion: use of Unchecked_Conversion;
• impure function: functions which write to variables other than parameters;
• recursive call: forbidden types of recursive calls, e.g. in contracts;
• uninitialized logic expr: expression which should be fully initialized;
• unsupported construct: any other unsupported construct.

As an example, consider the following code:

 package P is
    X : access Boolean;
    procedure P0;
 end P;

 package body P is
    procedure Set is
    begin
       X.all := True;
    end Set;

    procedure P0 is
       Y : Boolean;

       function Get return Boolean is
       begin
          return X.all;
       end Get;

       procedure P1 is
       begin
          if not Get then
             return;
          end if;
          Y := True;
       end P1;
    begin
       Set;
       P1;
    end P0;
 end P;

On this code, GNATprove outputs the following information in file p.alfa:

-+ set p.adb:2 (access)
-+ get p.adb:10 (access)
++ p1 p.adb:15
-+ p0 p.ads:3 (access)

The first character denotes whether the subprogram body is in SPARK 2014 (+), not in SPARK 2014 (-) or not yet implemented (*). The second character follows the same categories for the subprogram spec. The name that follows is a unique name for the subprogram. The location of the subprogram is given next with its file and line. Non-SPARK 2014 features used are given in parentheses. Features not yet implemented are given in brackets.

In the example above, Set and Get have a spec in SPARK 2014, but not their body, because it contains a pointer dereference. Since Set is a local subprogram of P0, the body of P0 is not in SPARK 2014 either. P1 body is in SPARK 2014.

Error Messages

This section lists the different error messages and warnings which GNATprove may output. Each message points to a very specific place in the source code. For example, if a source file file.adb contains a division as follows:

if X / Y > Z then ...

GNATprove may output a message such as:

file.adb:12:37: division check not proved

where the division sign / is precisely on line 12, column 37. Looking at the explanation in the first table below, which states that a division check verifies that the divisor is different from zero, it is clear that the message is about Y, and that GNATprove was unable to prove that Y cannot be zero. The explanations in the table below should be read with the context that is given by the source location.

The left column of the table contains the tag for each error message. Using option --show-tag, GNATprove prints the tag for each error message at the end of the message, in brackets.

The following table shows the proof messages.

Message Tag	Explanation
division_check	Check that the second operand of the division, mod or rem operation is different from zero.
index_check	Check that the given index is within the bounds of the array.
overflow_check	Check that the result of the given arithmetic operation is within the bounds of the base type.
range_check	Check that the given value is within the bounds of the expected scalar subtype.
length_check	Check that the given array is of the length of the expected array subtype.
discriminant_check	Check that the discriminant of the given discriminant record has the expected value. For variant records, this can happen for a simple access to a record field. But there are other cases where a fixed value of the discriminant is required.
precondition	Check that the precondition aspect of the given call evaluates to True.
postcondition	Check that the postcondition aspect of the subprogram evaluates to True.
contract_case	Check that all cases of the contract case evaluate to true at the end of the subprogram.
disjoint_contract_cases	Check that the cases of the contract cases aspect are all mutually disjoint.
complete_contract_cases	Check that the cases of the contract cases aspect cover the state space that is allowed by the precondition aspect.
loop_invariant_initialization	Check that the loop invariant evaluates to True on the first iteration of the loop.
loop_invariant_preservation	Check that the loop invariant evaluates to True at each further iteration of the loop.
loop_variant	Check that the given loop variant decreases/increases as specified during each iteration of the loop. This implies termination of the loop.
assertion	Check that the given assertion evaluates to True.

The following table shows the flow messages.

Todo

Add table with flow messages

How to Write Loop Invariants

Todo

Add section on how to write loop invariants

How to Investigate Unproved Checks

One of the most challenging aspects of formal verification is the analysis of failed proofs. If GNATprove fails to prove automatically that a run-time check or an assertion holds, there might be various reasons:

• [CODE] The check or assertion does not hold, because the code is wrong.
• [ASSERT] The assertion does not hold, because it is incorrect.
• [SPEC] The check or assertion cannot be proved, because of some missing assertions about the behavior of the program.
• [TIMEOUT] The check or assertion is not proved because the prover timeouts.
• [PROVER] The check or assertion is not proved because the prover is not smart enough.

Investigating Incorrect Code or Assertion

The first step is to check whether the code is incorrect [CODE] or the assertion is incorrect [ASSERT], or both. Since run-time checks and assertions can be executed at run time, one way to increase confidence in the correction of the code and assertions is to test the program on representative inputs. The following GNAT switches can be used:

• -gnato: enable run-time checking of intermediate overflows
• -gnat-p: reenable run-time checking even if -gnatp was used to suppress all checks
• -gnata: enable run-time checking of assertions

Investigating Unprovable Properties

The second step is to consider whether the property is provable [SPEC]. A check or assertion might be unprovable because a necessary annotation is missing:

• the precondition of the enclosing subprogram might be too weak; or
• the postcondition of a subprogram called might be too weak; or
• a loop invariant for an enclosing loop might be too weak; or
• a loop invariant for a loop before the check or assertion might be too weak.

In particular, GNATprove does not look into subprogram bodies, so all the necessary information for calls should be explicit in the subprogram contracts. A focused manual review of the code and assertions can efficiently diagnose many cases of missing annotations. Even when an assertion is quite large, GNATprove precisely locates the part that it cannot prove, which can help figuring out the problem. It may useful to simplify the code during this investigation, for example by adding a simpler assertion and trying to prove it.

GNATprove provides path information that might help the code review. Select Prove --> Show Path as described in Running GNATprove from GPS to display inside the editor the path on which the proof failed. In many cases, this is sufficient to spot a missing assertion. To further assist the user, we plan to add to this path some information about the values taken by variables from a counterexample.

Path displayed in GPS for an unproved property

Investigating Prover Shortcomings

The last step is to investigate if the prover would find a proof given enough time [TIMEOUT] or if another prover can find a proof [PROVER]. To that end, GNATprove provides options -timeout and -prover, usable either from the command-line (see Command-line Options) or inside GPS (see Running GNATprove from GPS).

Note that for the above experiments, it is quite convenient to use the Prove Line or Prove Subprogram features in GPS, as described in Running GNATprove from GPS, to get faster results for the desired line or subprogram.

A common limitation of automatic provers is that they don’t handle well non-linear arithmetic. For example, they might fail to prove simple checks involving multiplication, division, modulo or exponentiation.

In that case, a user may either:

• manually review the unproved checks and record that they can be trusted (for example by storing the result of GNATprove under version control), or
• add an assumption in the code to help the prover, in the form of a pragma Assume. GNATprove handles it like an assertion, so it both attempts to prove it, and uses it in subsequent code. If the assumption is not proved, it can be manually reviewed like mentioned above, and marking it as an assumption in the code helps documenting it.

We plan to provide a user view of the formula passed to the prover, for advanced users to inspect. This view will express in an Ada-like syntax the actual formula whose proof failed, to make it easier for users to interpret it. This format is yet to be defined.

For very advanced users, in particular those who would like to do manual proof of VCs, we will provide a description of the format of the VCs generated by GNATprove, so that users can understand the actual VCs passed to the prover. Each VC is stored in an individual file under the sub-directory gnatprove of the project object directory (default is the project directory). The file name follows the convention:

<file>_<line>_<column>_<check>_<num>.why

where:

• file is the name of the Ada source file for the check or assertion
• line is the line where the check or assertion appears
• column is the column
• check is an identifier for the check or assertion
• num is an optional number and identifies different paths through the program, between the start of the subprogram and the location of the check or assertion

For example, the VCs for a range check at line 160, column 42, of the file f.adb are stored in:

f.adb_160_42_range_check.why
f.adb_160_42_range_check_2.why
f.adb_160_42_range_check_3.why
...

The syntax of these files depend on the prover that was used. By default, it is Alt-Ergo, so these files are in Why3 proof syntax.

To be able to inspect these files, you should instruct GNATprove to keep them around by adding the switch -d to GNATprove‘s command line. You can also use the switch -v to get a detailed log of which VCs GNATprove is producing and attempting to prove.

GNATprove by Example

GNATprove is based on advanced technology for modular static analysis and deductive verification. It is very different both from compilers, which do very little analysis of the code, and static analyzers, which execute symbolically the program. GNATprove does a very powerful local analysis of the program, but it does not cross subprogram boundaries. Instead, it uses the subprogram contracts provided by users to interpret the effect of calls. Thus, it is essential to understand how GNATprove uses contracts, as well as other forms of annotations. This section aims at providing a deeper insight into how GNATprove formal verification works, through a step-by-step exploration of simple code examples.

Basic Examples

This section presents the results of running GNATprove on simple subprograms composed of assignments and branches.

Scalar Assignment

GNATprove is able to follow very precisely the assignments to scalar variables throughout the program. Take a very simple program Increment that assigns the value X+1 to the variable X:

package body T1Q1A
is

  procedure Increment (X: in out Integer)
  is
  begin
    X := X + 1;
  end Increment;

end T1Q1A;

The proof results show that GNATprove is unable to prove the overflow check on line 7, where X is incremented. This is not surprising, given that the initial value of X could be Integer'Last and incrementing it would indeed cause an overflow in this case.

t1q1a.adb:7:12: overflow check not proved

We can guard against this possibility by adding a suitable precondition to the specification of Increment. This states that that X must always be strictly less than Integer'Last at the point where the subprogram is called.

package T1Q1B
is

  procedure Increment (X: in out Integer)
    with Pre => X < Integer'Last;

end T1Q1B;

GNATprove assumes that the precondition holds when it performs the proof of Increment. For any subprogram which calls Increment, GNATprove will check that the precondition holds at the point of the call.

t1q1b.adb:7:13: info: overflow check proved

Swap

In the previous example GNATprove was able to prove that the subprogram was free from run-time exceptions but it did not help us with the question of whether the subprogram performed its intended function. Why not? Because we did not provide any specification of what the subprogram is supposed to do. We can specify properties about the required results of subprograms by adding postconditions to them, then using GNATprove to check that those postconditions hold.

To illustrate the use of postconditions, consider the subprogram Swap which exchanges the values of its two parameters X and Y. The Post aspect states that the new value of X will be the initial value of Y and vice-versa. Note the use of the 'Old attribute to refer to the initial values of the parameters.

package T1Q3A
is

  procedure Swap (X, Y : in out Integer)
   with Post => (X = Y'Old)
                  and then (Y = X'Old);

end T1Q3A;

The body of Swap makes use of a temporary variable to exchange the values of X and Y in the standard way.

package body T1Q3A
is

  procedure Swap (X, Y: in out Integer)
  is
     Temp: Integer;
  begin
     Temp := X;
     X := Y;
     Y := Temp;
  end Swap;

end T1Q3A;

The proof results show that GNATprove is able to prove that the postcondition holds.

t1q3a.ads:5:17: info: postcondition proved

NAND

Now we turn to a procedure NandGate which calculates the NAND of two Boolean values. Here the programmer has decided to specify the postcondition by enumerating all the entries in the truth table for a NAND function. This could have been written using the Post aspect like this:

with Post => ((if ((not P) and (not Q)) then R) and
              (if ((not P) and Q) then R) and
              (if (P and (not Q)) then R) and
              (if (P and Q) then (not R)));

However, the Contract_Cases aspect provides a convenient way to write this type of postcondition, as shown below:

package T1Q3B
is

  procedure NandGate(P,Q: in Boolean; R: out Boolean)
    with Contract_Cases => (not P and not Q => R,
                            not P and     Q => R,
                                P and not Q => R,
                                P and     Q => not R);

end T1Q3B;

The implementation is much simpler than the specification. This simplified expression for NAND could have been used in the specification as they are equivalent, but our programmer wanted to use the more efficient form in the implementation whilst keeping the more explicit version in the specification.

package body T1Q3B
is

  procedure NandGate (P, Q: in Boolean; R: out Boolean)
  is
  begin
     R := not (P and Q);
  end NandGate;

end T1Q3B;

The proof results show that GNATprove is able to prove that the postcondition holds, thus demonstrating that the simple expression in the body does indeed implement a NAND function. Note how the results show that each individual contract case was proved and that the overall contract was proved.

t1q3b.ads:5:45: info: contract case proved
t1q3b.ads:6:45: info: contract case proved
t1q3b.ads:7:45: info: contract case proved
t1q3b.ads:8:45: info: contract case proved
t1q3b.ads:5:10: info: disjoint contract cases proved
t1q3b.ads:5:10: info: complete contract cases proved

NextDay

The next example shows two subprograms, NextDay_A and NextDay_B, both of which have the same postcondition. Given a value of the enumeration type Day they will give the value of the next day. Naturally, this wraps around so if the day is Sunday (the last value in the enumeration) then the next day is Monday (the first value).

package T1Q3C
is

  type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);

  procedure NextDay_A(Today: in Day; Tomorrow: out Day)
    with Post => (Today=Mon and Tomorrow=Tue) or else
                 (Today=Tue and Tomorrow=Wed) or else
                 (Today=Wed and Tomorrow=Thu) or else
                 (Today=Thu and Tomorrow=Fri) or else
                 (Today=Fri and Tomorrow=Sat) or else
                 (Today=Sat and Tomorrow=Sun) or else
                 (Today=Sun and Tomorrow=Mon);

  procedure NextDay_B(Today: in Day; Tomorrow: out Day)
    with Post => (Today=Mon and Tomorrow=Tue) or else
                 (Today=Tue and Tomorrow=Wed) or else
                 (Today=Wed and Tomorrow=Thu) or else
                 (Today=Thu and Tomorrow=Fri) or else
                 (Today=Fri and Tomorrow=Sat) or else
                 (Today=Sat and Tomorrow=Sun) or else
                 (Today=Sun and Tomorrow=Mon);

end T1Q3C;

The bodies of the two subprograms illustrate two alternative implementations of the next day functionality. The first one uses the 'Succ attribute to get the next day, with a special case for Sunday as it is the last value in the type. The second version uses a case statement to state explicitly what the output should be for each input.

package body T1Q3C
is

  procedure NextDay_A (Today: in Day; Tomorrow: out Day)
  -- This is implementation (a) of NextDay, in which Day'Succ is used
  is
  begin
     if Today = Sun then
        Tomorrow := Mon;
     else
        Tomorrow := Day'Succ(Today);
     end if;
  end NextDay_A;

  procedure NextDay_B (Today: in Day; Tomorrow: out Day)
  -- This is implementation (b) of NextDay, in which a case-statement is used
  is
  begin
     case Today is
       when Mon => Tomorrow := Tue;
       when Tue => Tomorrow := Wed;
       when Wed => Tomorrow := Thu;
       when Thu => Tomorrow := Fri;
       when Fri => Tomorrow := Sat;
       when Sat => Tomorrow := Sun;
       when Sun => Tomorrow := Mon;
     end case;
  end NextDay_B;

end T1Q3C;

The proof results show that GNATprove is able to prove that both implementations meet their postconditions. There is also a range check on line 11, because the use of the 'Succ attribute could potentially cause a run-time error if Today is the last value in the type. However, the if statement guards against this so the check is proved.

t1q3c.adb:11:30: info: range check proved
t1q3c.ads:7:18: info: postcondition proved
t1q3c.ads:16:18: info: postcondition proved

Bounded_Addition

The procedure Bounded_Add takes two Integer values and calculates their sum. If the result would exceed the bounds of the Integer type then it should saturate at the maximum or minimum Integer value. The Contract_Cases aspect gives a natural way to express this specification.

package T1Q5
is

   procedure Bounded_Add (X, Y : in Integer; Z : out Integer)
     with Contract_Cases => (Integer'First <= X + Y and X + Y <= Integer'Last => Z = X + Y,
                             Integer'First > X + Y => Z = Integer'First,
                             X + Y > Integer'Last => Z = Integer'Last);

end T1Q5;

The tricky part is to implement this in the body without making use of a type that is larger than Integer. (If the implementation simply added the two values together to see if the result exceeded the bounds of Integer then it would obviously need a larger type to store the result.)

package body T1Q5
is

  procedure Bounded_Add (X, Y : in Integer; Z : out Integer)
  is
  begin
     if X < 0 and Y < 0 then -- both negative

        if X < Integer'First - Y then
           Z := Integer'First;
        else
           Z := X + Y;
        end if;

     elsif X > 0 and Y > 0 then -- both positive

        if X > Integer'Last - Y then
           Z := Integer'Last;
        else
           Z := X + Y;
        end if;

     else -- one +ve, one -ve: must be safe to add them

        Z := X + Y;

     end if;
  end Bounded_Add;

end T1Q5;

The proof results show that GNATprove is able to prove all the checks for this subprogram, so it satisifes its postcondition and there are no run-time errors. You may be wondering how it is that the postcondition in the subprogram specification contains an expression which simply adds together the two Integers, yet this does not overflow. This is because the project file specifies the compiler switch -gnato13 to define the semantics when calculating intermediate expressions. The first digit specifies the semantics for general code, with 1 meaning that the normal Ada type system semantics should be used. The second digit specifies the semantics for use in proof (preconditions, postconditions, assertions, invariants), with 3 meaning that mathematical semantics are used so there is no possibility of overflow. If this option were changed to -gnato11 then the normal Ada type system semantics would be used in proof expressions and GNATprove would (quite rightly) not be able to prove that there was no possibility of overflow in the postcondition. This is an important option and we recommend that users read the documentation carefully in order to understand how it behaves.

t1q5.adb:9:30: info: overflow check proved
t1q5.adb:12:19: info: overflow check proved
t1q5.adb:17:29: info: overflow check proved
t1q5.adb:20:19: info: overflow check proved
t1q5.adb:25:16: info: overflow check proved
t1q5.ads:5:79: info: contract case proved
t1q5.ads:6:52: info: contract case proved
t1q5.ads:7:51: info: contract case proved
t1q5.ads:5:11: info: disjoint contract cases proved
t1q5.ads:5:11: info: complete contract cases proved

Call Examples

This section presents the results of running GNATprove on subprograms calling other subprograms.

Increment Revisited

Earlier on we saw a procedure Increment which takes an Integer X and increments it by 1. In order to prove that the statement which adds 1 to X cannot result in an overflow we specified the precondition that X < Integer'Last. To see how this precondition is used, let’s consider a procedure Add2 which adds two to an Integer by making multiple calls to Increment.

package body T1Q1C
is

  procedure Increment (X : in out Integer)
  is
  begin
     X := X + 1;
  end Increment;

  procedure Add2 (X : in out Integer)
  is
  begin
     Increment (X);
     Increment (X);
  end Add2;

end T1Q1C;

If we try to prove this with GNATprove it reports the following:

t1q1c.adb:13:6: precondition not proved
t1q1c.adb:14:6: precondition not proved
t1q1c.adb:7:13: info: overflow check proved

For each call to Increment we are required to show that its precondition holds, i.e. X must be strictly less than Integer'Last. One possible approach here would be to guard each call to Increment with an if statement so that it is only called it the precondition is met. This would make Add2 saturate at Integer'Last. However, the specification of Add2 has a postcondition stating that it must always increase the value of X by two. The programmer discussed this postcondition with the system designers and determined that it is fundamental to the correct operation of the overall program so it cannot be changed. Therefore the right thing to do here is add a suitable precondition to Add2.

package T1Q1D
is

  procedure Increment (X: in out Integer)
    with Pre => X < Integer'Last;

  procedure Add2 (X : in out Integer)
    with Pre => X <= Integer'Last - 2,
         Post => X = X'Old + 2;

end T1Q1D;

Having added this precondition, GNATprove is able to prove that the precondition on the first call to Increment always holds, but it fails to prove it for the second call, and it fails to prove the postcondition on Add2. What’s going on?

t1q1d.adb:7:13: info: overflow check proved
t1q1d.adb:13:6: info: precondition proved
t1q1d.adb:14:6: precondition not proved
t1q1d.ads:9:18: postcondition not proved, requires X = X'Old + 2

The trouble is that there is no postcondition specified for Increment so GNATprove knows nothing about the value of X after each call to Increment (other than that it is in the range of Integer). So let’s add a postcondition to Increment saying what it does.

package T1Q1E
is

  procedure Increment (X: in out Integer)
    with Pre => X < Integer'Last,
         Post => X = X'Old + 1;

  procedure Add2 (X : in out Integer)
    with Pre => X <= Integer'Last - 2,
         Post => X = X'Old + 2;

end T1Q1E;

Now GNATprove is able to prove all the checks and contracts.

t1q1e.adb:7:13: info: overflow check proved
t1q1e.ads:6:18: info: postcondition proved
t1q1e.adb:13:6: info: precondition proved
t1q1e.adb:14:6: info: precondition proved
t1q1e.ads:10:18: info: postcondition proved

Loop Examples

This section presents the results of running GNATprove on subprograms containing loops.

Integer Square Root

IntSqrt

The procedure ISQRT calculates the integer square root of a natural number. The postcondition specifies that the required result Root must have a value such that Root squared is less than or equal to the input value but Root + 1 squared must be strictly greater than the input value.

package T1Q4
is

   procedure ISQRT(N: in Natural; Root: out Natural)
     with Post => (Root*Root <= N and
                     (Root+1)*(Root+1) > N);

end T1Q4;

The implementation in the body is not particularly efficient! It simply starts at 0 and increments the potential answer by 1 each time around the loop until it finds a value that satisfies the specification. In order to prove properties about code involving loops it is normally necessary to provide a loop invariant. In GNATprove this is done by means of the pragma Loop_Invariant which, in this case, states that the current candidate answer Local_Root squared is less than or equal to the input value N and is less than or equal to Natural'Last. Note the use of the larger type Big_Natural which has been introduced because the result of squaring a Natural could clearly exceed the range of the type Natural. Observe that the invariant has been placed just before the end of the loop as this is the natural place for it in this particular example - there is no need for invariants to be placed right at the top of loops.

package body T1Q4
is

   procedure ISQRT (N: in Natural; Root: out Natural)
   is
      -- Introduce a new subtype to use to avoid possible overflow
      -- of expression in loop exit statement.
      subtype Big_Natural is Long_Long_Integer range 0 .. Long_Long_Integer'Last;

      Local_Root : Big_Natural;

   begin
      Local_Root := 0;

      loop
          exit when (Local_Root + 1) * (Local_Root + 1) > Big_Natural (N);

          Local_Root := Local_Root + 1;

         -- Loop Invariant is in terms of the incremented value of Local_Root.
         pragma Loop_Invariant
           (Local_Root * Local_Root <= Big_Natural(N)
            and then Local_Root <= Big_Natural(Natural'Last));

      end loop;

      Root := Natural(Local_Root);
   end ISQRT;
end T1Q4;

The proof results show that GNATprove is able to prove all the checks for the loop invariant (which must be shown to hold for the path leading into the loop, and for the path back around the loop), the postcondition, and for overflow and range checks.

t1q4.adb:16:33: info: overflow check proved
t1q4.adb:16:38: info: overflow check proved
t1q4.adb:16:52: info: overflow check proved
t1q4.adb:18:36: info: overflow check proved
t1q4.adb:21:10: info: loop invariant initialization proved
t1q4.adb:21:10: info: loop invariant preservation proved
t1q4.adb:27:23: info: range check proved
t1q4.ads:5:19: info: postcondition proved

SumArray

Here is a more complex loop example, this time using a for loop. The function SumArray calculates the sum of the values of the elements of an array. The array has 100 elements, each of which may be in the range 0 to 1000. A suitable subtype has been defined to store the result.

package T3Q4
is

   subtype ElementType is Natural range 0..1000;
   subtype IndexType is Positive range 1..100;
   type ArrayType is array (IndexType) of ElementType;
   subtype SumType is Natural range 0..100000;

   function SumArray (A : in ArrayType) return SumType;

end T3Q4;

The loop invariant states that the current value of the sum is equal to the sum of the elements that have been iterated over so far, and cannot be more than 1000 times the number of elements iterated over so far. The expression function Summed_Between has been defined to help with this and is needed for proof purposes only as it only appears in the loop invariant.

package body T3Q4
is

   -- Summed_Between is needed for proof purposes only
   function Summed_Between (A : in ArrayType;
                            L, U : in IndexType) return SumType
    with Pre  => (L <= U),
         Post => (Summed_Between'Result <= (U - L + 1) * 1000);

   function Summed_Between (A : in ArrayType;
                            L, U : in IndexType) return SumType is
      (if (L = U) then A(L)
       elsif (L < U) then Summed_Between (A, L, U - 1) + A (U)
       else 0);

   function SumArray (A : in ArrayType) return SumType
   is
      Sum : SumType := 0;
   begin
      for I in IndexType loop
        pragma Loop_Invariant ((if I /= IndexType'First then Sum = Summed_Between(A, IndexType'First, I - 1)) and
          Sum <= 1000 * (I - IndexType'First));
        Sum := Sum + A (I);
     end loop;
     return Sum;
   end SumArray;

end T3Q4;

The proof results show that GNATprove is able to prove all checks for this example.

t3q4.adb:8:18: info: postcondition proved
t3q4.adb:13:27: info: precondition proved
t3q4.adb:13:51: info: range check proved
t3q4.adb:13:56: info: range check proved
t3q4.adb:21:9: info: loop invariant initialization proved
t3q4.adb:21:9: info: loop invariant preservation proved
t3q4.adb:21:68: info: precondition proved
t3q4.adb:21:105: info: range check proved
t3q4.adb:23:20: info: range check proved