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.