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).

.. index:: Initializes; automatic generation

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:

.. literalinclude:: /examples/ug__init_data/external_data.ads
   :language: ada
   :linenos:

.. literalinclude:: /examples/ug__init_data/init_data.ads
   :language: ada
   :linenos:

.. literalinclude:: /examples/ug__init_data/init_data.adb
   :language: ada
   :linenos:

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

.. code-block:: ada

   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:

.. literalinclude:: /examples/ug__init_data/main_proc.adb
   :language: ada
   :linenos:

.. index:: speeding up; explicit package contracts

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 :ref:`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.
