Usage Scenarios for Formal Verification

To be completed

GNATprove generates Verification Conditions (VCs) whose proof ensures that some property holds on the source program. Such VCs are generated for functional properties expressed as annotations but also to ensure different high-level properties of the code described in the subsequent sections.

Completeness of Preconditions

This verification activity is part of the proof analysis of GNATprove. It consists in verifying that preconditions of subprograms can never raise a run-time error, whatever the calling context. In order to get such a good property on the preconditions, the user should in general guard all expressions which may raise a Constraint_Error in Ada, such as array accesses and arithmetic operations.

These guards may take the form desired by the user. In particular, no guard is necessary if the operation cannot raise a run-time error, e.g. due to the ranges of variables involved. As an example, consider the following subprogram specifications:

procedure Not_Guarded (X, Y : Integer) with
  Pre => X / Y > 0;

procedure Guarded_And_Then (X, Y : Integer) with
  Pre => Y /= 0 and then X / Y > 0;

procedure Guarded_If_Then (X, Y : Integer) with
  Pre => (if Y /= 0 then X / Y > 0);

procedure No_Need_For_Guard (X, Y : Positive) with
  Pre => X / Y > 0;

GNATprove is able to show that only the precondition of the first of these specifications could raise a run-time error:

p.ads:4:15: division check not proved
p.ads:7:31: (info) division check proved
p.ads:10:31: (info) division check proved
p.ads:13:15: (info) division check proved

Notice also that division might also overflow here, if X is the minimal integer value and Y is -1 (standard 32-bits integers are assumed here). GNATprove checks this overflow condition, and it detects that only the precondition of the last of these specifications cannot raise a run-time error:

p.ads:4:15: overflow check not proved
p.ads:7:31: overflow check not proved
p.ads:10:31: overflow check not proved
p.ads:13:15: (info) overflow check proved

Absence of Run-Time Errors

This verification activity is available in mode prove. GNATprove verifies that the code of a subprogram analyzed does not contain violations of the following checks:

• overflow check
• range check
• index check
• division check
• discriminant check
• length check

The precise meaning of these checks is given by the Ada Language Reference Manual. An (overflow check) violation occurs when the result of an arithmetic operation cannot be represented in the base type (usually a machine integer) for this operation. A (range check) violation occurs when a value does not respect the range constraint for its type. An (index check) violation occurs when the value used to index into an array does not fit between the array bounds. A (division check) violation occurs when the divisor of a division operation (or rem or mod) is zero. A discriminant check violation occurs when the discriminant(s) of a discriminant record does not have the expected value for a given operation. A length check violation occurs when an array does not have the expected length.

Note that GNATprove also takes into account checks that occur in assertions and pre- and postconditions.

Functional Verification

This verification activity is available in mode prove. GNATprove generates VCs to prove that all subprograms called in the code of a subprogram analyzed have their precondition satisfied at the point of call. It also generates VCs to prove that the postcondition of the subprogram analyzed is satisfied.

In order to prove such VCs, the user may have to write loop invariants, for which specific VCs are generated, to prove that the loop invariant is initially valid (loop invariant initiation) and that it is preserved through the loop (loop invariant preservation).