7.6. How to Write Package Contracts

Like for subprogram contracts, GNATprove can generate default package contracts when not specified by a user. By default, GNATprove does not require the user to write any package contracts.

The default state abstraction generated by GNATprove maps every internal global variable to a different internal abstract state (which is not really abstract as a result).

The default package initialization generated by GNATprove lists all variables initialized either at declaration or in the package body statements. The generated Initializes aspect is an over-approximation of the actual Initializes aspect. All outputs are considered to be initialized from all inputs. For example, consider package Init_Data which initializes all its global variables during elaboration, from either constants or variables:

1
2
3
4
5
package External_Data with
  SPARK_Mode
is
   Val : Integer with Import;
end External_Data;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
with External_Data;
pragma Elaborate_All(External_Data);

package Init_Data with
  SPARK_Mode
is
   pragma Elaborate_Body;
   Start_From_Zero     : Integer := 0;
   Start_From_Val      : Integer := External_Data.Val;
   Start_From_Zero_Bis : Integer;
   Start_From_Val_Bis  : Integer;
end Init_Data;

1
2
3
4
5
6
7
package body Init_Data with
  SPARK_Mode
is
begin
   Start_From_Zero_Bis := 0;
   Start_From_Val_Bis  := External_Data.Val;
end Init_Data;

GNATprove generates a package initialization contract on package Init_Data which is equivalent to:

Initializes => (Start_From_Zero     => External_Data.Val,
                Start_From_Zero_Bis => External_Data.Val,
                Start_From_Val      => External_Data.Val,
                Start_From_Val_Bis  => External_Data.Val)

As a result, GNATprove can check that global variables are properly initialized when calling the main procedure Main_Proc, and it does not issue any message when analyzing this code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
with Init_Data;
procedure Main_Proc with
  SPARK_Mode
is
   Tmp : Integer;
begin
   Tmp := Init_Data.Start_From_Zero;
   Tmp := Init_Data.Start_From_Val;
   Tmp := Init_Data.Start_From_Zero_Bis;
   Tmp := Init_Data.Start_From_Val_Bis;
end Main_Proc;

The user may specify explicitly package contracts to:

  • name explicitly the parts of state abstraction that can be used in subprogram dependency contracts, in order to Address Data and Control Coupling; or

  • improve scalability and running time of GNATprove’s analysis, as a single explicit abstract state may be mapped to hundreds of concrete global variables, which would otherwise be considered separately in the analysis; or

  • check that initialization of global data at elaboration is as specified in the specified package initialization contracts.