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:

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

 1with External_Data;
 2pragma Elaborate_All(External_Data);
 3
 4package Init_Data with
 5  SPARK_Mode
 6is
 7   pragma Elaborate_Body;
 8   Start_From_Zero     : Integer := 0;
 9   Start_From_Val      : Integer := External_Data.Val;
10   Start_From_Zero_Bis : Integer;
11   Start_From_Val_Bis  : Integer;
12end Init_Data;

1package body Init_Data with
2  SPARK_Mode
3is
4begin
5   Start_From_Zero_Bis := 0;
6   Start_From_Val_Bis  := External_Data.Val;
7end 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:

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