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.