7.9.1. Basic Examples

The examples in this section have no loops, and do not use more complex features of SPARK like Ghost Code, Interfaces to the Physical World, or Object Oriented Programming and Liskov Substitution Principle.

7.9.1.1. Increment

Consider a simple procedure that increments its integer parameter X:

1
2
3
4
5
6
procedure Increment (X : in out Integer) with
  SPARK_Mode
is
begin
   X := X + 1;
end Increment;

As this procedure does not have a contract yet, GNATprove only checks that there are no possible reads of uninitialized data and no possible run-time errors in the procedure. Here, it issues a message about a possible overflow check failure on X + 1:

increment.adb:5:11: medium: overflow check might fail (e.g. when X = 2147483647)

The counterexample displayed tells us that Increment could be called on value Integer'Last for parameter X, which would cause the increment to raise a run-time error. One way to eliminate this vulnerability is to add a precondition to Increment specifying that X should be less than Integer'Last when calling the procedure:

1
2
3
4
5
6
7
procedure Increment_Guarded (X : in out Integer) with
  SPARK_Mode,
  Pre => X < Integer'Last
is
begin
   X := X + 1;
end Increment_Guarded;

As this procedure has a contract now, GNATprove checks like before that there are no possible reads of uninitialized data and no possible run-time errors in the procedure, including in its contrat, and that the procedure implements its contract. As expected, GNATprove now proves that there is no possible overflow check failure on X + 1:

increment_guarded.adb:6:11: info: overflow check proved

The precondition is usually the first contract added to a subprogram, but there are other Subprogram Contracts. Here is a version of Increment with:

  • global dependencies (aspect Global) stating that the procedure reads and writes no global variables
  • flow dependencies (aspect Depends) stating that the final value of parameter X only depends on its input value
  • a precondition (aspect Pre) stating that parameter X should be less than Integer'Last on entry
  • a postcondition (aspect Post) stating that parameter X should have been incremented by the procedure on exit
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
procedure Increment_Full (X : in out Integer) with
  SPARK_Mode,
  Global  => null,
  Depends => (X => X),
  Pre     => X < Integer'Last,
  Post    => X = X'Old + 1
is
begin
   X := X + 1;
end Increment_Full;

GNATprove checks that Increment_Full implements its contract, and that it cannot raise run-time errors or read uninitialized data. By default, GNATprove‘s output is empty in such a case, but we can request that it prints one line per check proved by using switch --report=all, which we do here:

increment_full.adb:6:14: info: postcondition proved
increment_full.adb:6:24: info: overflow check proved
increment_full.adb:9:11: info: overflow check proved

As subprogram contracts are used to analyze callers of a subprogram, let’s consider a procedure Increment_Calls that calls the different versions of Increment presented so far:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
with Increment;
with Increment_Guarded;
with Increment_Full;

procedure Increment_Calls with
  SPARK_Mode
is
   X : Integer;
begin
   X := 0;
   Increment (X);
   Increment (X);

   X := 0;
   Increment_Guarded (X);
   Increment_Guarded (X);

   X := 0;
   Increment_Full (X);
   Increment_Full (X);
end Increment_Calls;

GNATprove proves all preconditions expect the one on the second call to Increment_Guarded:

increment_calls.adb:11:15: info: initialization of "X" proved
increment_calls.adb:12:15: info: initialization of "X" proved
increment_calls.adb:15:04: info: precondition proved
increment_calls.adb:15:23: info: initialization of "X" proved
increment_calls.adb:16:04: medium: precondition might fail (e.g. when X = 2147483647)
increment_calls.adb:16:23: info: initialization of "X" proved
increment_calls.adb:19:04: info: precondition proved
increment_calls.adb:19:20: info: initialization of "X" proved
increment_calls.adb:20:04: info: precondition proved
increment_calls.adb:20:20: info: initialization of "X" proved

Increment has no precondition, so there is nothing to check here except the initialization of X when calling Increment on lines 11 and 12. But remember that GNATprove did issue a message about a true vulnaribility on Increment‘s implementation.

This vulnerability was corrected by adding a precondition to Increment_Guarded. This has the effect of pushing the constraint on callers, here procedure Increment_Calls. As expected, GNATprove proves that the first call to Increment_Guarded on line 15 satisfies its precondition. But it does not prove the same for the second call to Increment_Guarded on line 16, because the value of X on line 16 was set by the call to Increment_Guarded on line 15, and the contract of Increment_Guarded does not say anything about the possible values of X on exit.

Thus, a postcondition like the one on Increment_Full is needed so that GNATprove can check the second call to increment X. As expected, GNATprove proves that both calls to Increment_Full on lines 19 and 20 satisfy their precondition.

In some cases, the user is not interested in specifying and verifying a complete contract like the one on Increment_Full, typically for helper subprograms defined locally in a subprogram or package body. GNATprove allows performing Contextual Analysis of Subprograms Without Contracts for these local subprograms. For example, consider a local definition of Increment inside procedure Increment_Local:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
procedure Increment_Local with
  SPARK_Mode
is
   procedure Increment (X : in out Integer) is
   begin
      X := X + 1;
   end Increment;

   X : Integer;

begin
   X := 0;
   Increment (X);
   Increment (X);
   pragma Assert (X = 2);
end Increment_Local;

Although Increment has no contract (like the previous non-local version), GNATprove proves that this program is free from run-time errors, and that the assertion on line 15 holds:

increment_local.adb:6:12: info: initialization of "X" proved, in call inlined at increment_local.adb:13
increment_local.adb:6:12: info: initialization of "X" proved, in call inlined at increment_local.adb:14
increment_local.adb:6:14: info: overflow check proved, in call inlined at increment_local.adb:13
increment_local.adb:6:14: info: overflow check proved, in call inlined at increment_local.adb:14
increment_local.adb:15:19: info: assertion proved
increment_local.adb:15:19: info: initialization of "X" proved

7.9.1.2. Swap

Consider a simple procedure that swaps its integer parameters X and Y, whose simple-minded implementation is wrong:

1
2
3
4
5
6
7
procedure Swap_Bad (X, Y : in out Integer) with
  SPARK_Mode
is
begin
   X := Y;
   Y := X;
end Swap_Bad;

As this procedure does not have a contract yet, GNATprove only checks that there are no possible reads of uninitialized data and no possible run-time errors in the procedure. Here, it simply issues a warning:

swap_bad.adb:1:21: warning: unused initial value of "X"

But we know the procedure is wrong, so we’d like to get an error of some sort! We could not detect it with GNATprove because the error is functional, and GNATprove cannot guess the intended functionality of Swap_Bad. Fortunately, we can give this information to GNATprove by adding a contract to Swap_Bad.

One such contract is the flow dependencies introduced by aspect Depends. Here it specifies that the final value of X (resp. Y) should depend on the initial value of Y (resp. X):

1
2
3
4
5
6
7
8
procedure Swap_Bad_Depends (X, Y : in out Integer) with
  SPARK_Mode,
  Depends => (X => Y, Y => X)
is
begin
   X := Y;
   Y := X;
end Swap_Bad_Depends;

GNATprove issues 3 check messages on Swap_Bad_Depends:

swap_bad_depends.adb:1:29: warning: unused initial value of "X"
swap_bad_depends.adb:3:03: medium: missing dependency "null => X"
swap_bad_depends.adb:3:23: medium: missing dependency "Y => Y"
swap_bad_depends.adb:3:28: medium: incorrect dependency "Y => X"

The last message informs us that the dependency Y => X stated in Swap_Bad_Depends‘s contract is incorrect for the given implementation. That might be either an error in the code or an error in the contract. Here this is an error in the code. The two other messages are consequences of this error.

Another possible contract is the postcondition introduced by aspect Post. Here it specifies that the final value of X (resp. Y) is equal to the initial value of Y (resp. X):

1
2
3
4
5
6
7
8
procedure Swap_Bad_Post (X, Y : in out Integer) with
  SPARK_Mode,
  Post => X = Y'Old and Y = X'Old
is
begin
   X := Y;
   Y := X;
end Swap_Bad_Post;

GNATprove issues one check message on the unproved postcondition of Swap_Bad_Post, with a counterexample giving concrete values of a wrong execution:

swap_bad_post.adb:3:25: medium: postcondition might fail, cannot prove Y = X'old (e.g. when X'Old = 1 and Y = 0)

Both the check messages on Swap_Bad_Depends and on Swap_Bad_Post inform us that the intended functionality as expressed in the contracts is not implemented in the procedure. And looking again at the warning issued by GNATprove on Swap_Bad, this was already pointing at the same issue: swapping the values of X and Y should obviously lead to reading the initial value of X; the fact that this value is not used is a clear sign that there is an error in the implementation. The correct version of Swap uses a temporary value to hold the value of X:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
procedure Swap (X, Y : in out Integer) with
  SPARK_Mode,
  Depends => (X => Y, Y => X),
  Post    => X = Y'Old and Y = X'Old
is
   Tmp : constant Integer := X;
begin
   X := Y;
   Y := Tmp;
end Swap;

GNATprove proves both contracts on Swap and it informs us that the postcondition was proved:

swap.adb:4:14: info: postcondition proved

Let’s now consider a well-known in place implementation of Swap that avoids introducing a temporary variable by using bitwise operations:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
with Interfaces; use Interfaces;

procedure Swap_Modulo (X, Y : in out Unsigned_32) with
  SPARK_Mode,
  Post => X = Y'Old and Y = X'Old
is
begin
   X := X xor Y;
   Y := X xor Y;
   X := X xor Y;
end Swap_Modulo;

GNATprove understands the bitwise operations on values of modular types, and it proves here that the postcondition of Swap_Modulo is proved:

swap_modulo.adb:5:11: info: postcondition proved

GNATprove‘s flow analysis issues warnings like the one on Swap_Bad whenever it detects that some variables or statements are not used in the computation, which is likely uncovering an error. For example, consider procedure Swap_Warn which assigns X and Tmp_Y out of order:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
procedure Swap_Warn (X, Y : in out Integer) with
  SPARK_Mode
is
   Tmp_X : Integer;
   Tmp_Y : Integer;
begin
   Tmp_X := X;
   X := Tmp_Y;
   Tmp_Y := Y;
   Y := Tmp_X;
end Swap_Warn;

On this wrong implementation, GNATprove issues a high check message for the certain read of an uninitialized variable, and two warnings that point to unused constructs:

swap_warn.adb:1:25: warning: unused initial value of "Y"
swap_warn.adb:8:09: high: "Tmp_Y" is not initialized
swap_warn.adb:8:09: warning: "Tmp_Y" may be referenced before it has a value
swap_warn.adb:9:10: warning: unused assignment
swap_warn.adb:10:09: info: initialization of "Tmp_X" proved

In general, warnings issued by GNATprove‘s flow analysis should be carefully reviewed, as they may lead to the discovery of errors in the program.

7.9.1.3. Addition

Consider a simple function Addition that returns the sum of its integer parameters X and Y. As in Increment, we add a suitable precondition and postcondition for this function:

1
2
3
4
5
6
7
8
9
function Addition (X, Y : Integer) return Integer with
  SPARK_Mode,
  Depends => (Addition'Result => (X, Y)),
  Pre     => X + Y in Integer,
  Post    => Addition'Result = X + Y
is
begin
   return X + Y;
end Addition;

We also added flow dependencies to Addition for illustration purposes, but they are the same as the default generated ones (the result of the function depends on all its inputs), so are not in general given explicitly.

GNATprove issues a check message about a possible overflow in the precondition of Addition:

addition.adb:4:16: medium: overflow check might fail (e.g. when X = -2147483648 and Y = -1)
addition.adb:5:14: info: postcondition proved
addition.adb:5:34: info: overflow check proved
addition.adb:8:13: info: overflow check proved

Indeed, if we call for example Addition on values Integer'Last for X and 1 for Y, the expression X + Y evaluated in the precondition does not fit in a machine integer and raises an exception at run time. In this specific case, some people may consider that it does not really matter that an exception is raised due to overflow as the failure of the precondition should also raise a run-time exception. But in general the precondition should not fail (just consider the precondition X + Y not in Integer for example), and even here, the different exceptions raised may be treated differently (Constraint_Error in the case of an overflow, Assertion_Error in the case of a failing precondition).

One way to avoid this vulnerability is to rewrite the precondition so that no overflow can occur:

1
2
3
4
5
6
7
8
9
function Addition_Rewrite (X, Y : Integer) return Integer with
  SPARK_Mode,
  Depends => (Addition_Rewrite'Result => (X, Y)),
  Pre     => (X >= 0 and then Y <= Integer'Last - X) or else (X < 0 and then Y >= Integer'First - X),
  Post    => Addition_Rewrite'Result = X + Y
is
begin
   return X + Y;
end Addition_Rewrite;

Although GNATprove proves that Addition_Rewrite implements its contract and is free from run-time errors, the rewritten precondition is not so readable anymore:

addition_rewrite.adb:4:49: info: overflow check proved
addition_rewrite.adb:4:97: info: overflow check proved
addition_rewrite.adb:5:14: info: postcondition proved
addition_rewrite.adb:5:42: info: overflow check proved
addition_rewrite.adb:8:13: info: overflow check proved

A better way to achieve the same goal without losing in readability is to execute and analyze contracts in a special mode where overflows cannot occur, as explained in Overflow Modes. In that case, GNATprove proves that there are no run-time errors in function Addition, and that it implements its contract.

Finally, we can choose to expand the range of applicability of the function, by accepting any values of inputs X and Y, and saturating when the addition would overflow the bounds of machine integers. That’s what function Addition_Saturated does, and its saturating behavior is expressed in Contract Cases:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
function Addition_Saturated (X, Y : Integer) return Integer with
  SPARK_Mode,
  Contract_Cases => ((X + Y in Integer)    => Addition_Saturated'Result = X + Y,
                     X + Y < Integer'First => Addition_Saturated'Result = Integer'First,
                     X + Y > Integer'Last  => Addition_Saturated'Result = Integer'Last)
is
begin
   if X < 0 and Y < 0 then -- both negative
      if X < Integer'First - Y then
         return Integer'First;
      else
         return X + Y;
      end if;

   elsif X > 0 and Y > 0 then -- both positive
      if X > Integer'Last - Y then
         return Integer'Last;
      else
         return X + Y;
      end if;

   else -- one positive or null, one negative or null, adding them is safe
      return X + Y;
   end if;
end Addition_Saturated;

GNATprove proves that Addition_Saturated implements its contract and is free from run-time errors:

addition_saturated.adb:3:03: info: complete contract cases proved
addition_saturated.adb:3:03: info: disjoint contract cases proved
addition_saturated.adb:3:44: info: contract case proved
addition_saturated.adb:4:44: info: contract case proved
addition_saturated.adb:5:44: info: contract case proved
addition_saturated.adb:9:28: info: overflow check proved
addition_saturated.adb:12:19: info: overflow check proved
addition_saturated.adb:16:27: info: overflow check proved
addition_saturated.adb:19:19: info: overflow check proved
addition_saturated.adb:23:16: info: overflow check proved

Note that we analyzed this function in ELIMINATED overflow mode, using the switch -gnato13, otherwise there would be possible overflows in the guard expressions of the contract cases.