# 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: high: overflow check might fail, cannot prove upper bound for X + 1
5 | X := X + 1;
| ~~^~~
e.g. when X = Integer'Last
reason for check: result of addition must fit in a 32-bits machine integer
possible fix: subprogram at line 1 should mention X in a precondition
1 |procedure Increment (X : in out Integer) with
|^ here
```

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. As suggested by the possible fix in the message
issued by GNATprove, 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 contract, 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 variablesflow dependencies (aspect

`Depends`

) stating that the final value of parameter`X`

only depends on its input valuea precondition (aspect

`Pre`

) stating that parameter`X`

should be less than`Integer'Last`

on entrya 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:3:03: info: data dependencies proved
increment_full.adb:4:03: info: flow dependencies proved
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:8:04: info: initialization of "X" proved
increment_calls.adb:15:04: info: precondition proved
increment_calls.adb:16:04: medium: precondition might fail
16 | Increment_Guarded (X);
| ^~~~~~~~~~~~~~~~~~~~
e.g. when X = Integer'Last
possible fix: call at line 15 should mention X (for argument X) in a postcondition
15 | Increment_Guarded (X);
| ^ here
increment_calls.adb:19:04: info: precondition proved
increment_calls.adb:20:04: info: precondition 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 vulnerability 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.

As suggested by the possible fix in the message issued by GNATprove,
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: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:9:04: info: initialization of "X" proved
increment_local.adb:15:19: info: assertion 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"
1 |procedure Swap_Bad (X, Y : in out Integer) with
| ^ here
```

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 (and a warning) on `Swap_Bad_Depends`

:

```
swap_bad_depends.adb:1:29: warning: unused initial value of "X"
1 |procedure Swap_Bad_Depends (X, Y : in out Integer) with
| ^ here
swap_bad_depends.adb:3:03: medium: missing dependency "null => X"
3 | Depends => (X => Y, Y => X)
| ^~~~~~~~~~~~~~~~~~~~~~~~~~
swap_bad_depends.adb:3:23: medium: missing self-dependency "Y => Y"
3 | Depends => (X => Y, Y => X)
| ^ here
swap_bad_depends.adb:3:28: medium: incorrect dependency "Y => X"
3 | Depends => (X => Y, Y => X)
| ^ here
```

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`

(and a warning), with a counterexample giving concrete values
of a wrong execution:

```
swap_bad_post.adb:1:26: warning: unused initial value of "X"
1 |procedure Swap_Bad_Post (X, Y : in out Integer) with
| ^ here
swap_bad_post.adb:3:25: high: postcondition might fail, cannot prove Y = X'old
3 | Post => X = Y'Old and 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:3:03: info: flow dependencies 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 three warnings that point to unused constructs:

```
swap_warn.adb:1:25: warning: unused initial value of "Y"
1 |procedure Swap_Warn (X, Y : in out Integer) with
| ^ here
swap_warn.adb:8:09: warning: "Tmp_Y" may be referenced before it has a value [enabled by default]
8 | X := Tmp_Y;
| ^~~~~
swap_warn.adb:8:09: high: "Tmp_Y" is not initialized
8 | X := Tmp_Y;
| ^~~~~
swap_warn.adb:9:10: warning: unused assignment
9 | Tmp_Y := Y;
| ~~~~~~^~~~
```

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: high: overflow check might fail, cannot prove lower bound for X + Y
4 | Pre => X + Y in Integer,
| ~~^~~
e.g. when X = Integer'First
and Y = -1
reason for check: result of addition must fit in a 32-bits machine integer
possible fix: use pragma Overflow_Mode or switch -gnato13 or unit Ada.Numerics.Big_Numerics.Big_Integers
```

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 (X, Y : Integer) return Integer with
SPARK_Mode,
Depends => (Addition'Result => (X, Y)),
Pre => (X >= 0 and then Y <= Integer'Last - X) or else (X < 0 and then Y >= Integer'First - X),
Post => Addition'Result = X + Y
is
begin
return X + Y;
end Addition;
``` |

Although GNATprove proves that `Addition`

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

```
addition.adb:3:03: info: flow dependencies proved
addition.adb:4:49: info: overflow check proved
addition.adb:4:97: info: overflow check proved
addition.adb:5:14: info: postcondition proved
addition.adb:5:34: info: overflow check proved
addition.adb:8:13: info: overflow check proved
```

A better way to achieve the same goal without losing in readability is to use the Big Numbers Library for arithmetic operations which could overflow:

1 2 3 4 5 6 7 8 9 10 11 | ```
with Ada.Numerics.Big_Numbers.Big_Integers;
use Ada.Numerics.Big_Numbers.Big_Integers;
function Addition (X, Y : Big_Integer) return Big_Integer with
SPARK_Mode,
Depends => (Addition'Result => (X, Y)),
Post => Addition'Result = X + Y
is
begin
return X + Y;
end Addition;
``` |

In that case, GNATprove proves that there are no run-time errors in function
`Addition`

, and that it implements its contract:

```
addition.adb:6:03: info: flow dependencies proved
addition.adb:7:14: info: postcondition proved
addition.adb:7:22: info: predicate check proved
addition.adb:7:32: info: predicate check proved
addition.adb:7:36: info: predicate check proved
addition.adb:10:11: info: predicate check proved
addition.adb:10:15: info: predicate check proved
```

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 the
rewritten function `Addition`

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 (X, Y : Integer) return Integer with
SPARK_Mode,
Contract_Cases => ((X + Y in Integer) => Addition'Result = X + Y,
X + Y < Integer'First => Addition'Result = Integer'First,
X + Y > Integer'Last => Addition'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;
``` |

GNATprove proves that `Addition`

implements its contract and is free from
run-time errors:

```
addition.adb:3:03: info: disjoint contract cases proved
addition.adb:3:03: info: complete contract cases proved
addition.adb:3:44: info: contract case proved
addition.adb:4:44: info: contract case proved
addition.adb:5:44: info: contract case proved
addition.adb:9:28: info: overflow check proved
addition.adb:12:19: info: overflow check proved
addition.adb:16:27: info: overflow check proved
addition.adb:19:19: info: overflow check proved
addition.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.