SPARK 2005 to SPARK 2014 Mapping Specification ============================================== This appendix defines the mapping between SPARK 2005 and |SPARK|. It is intended as both a completeness check for the |SPARK| language design, and as a guide for projects upgrading from SPARK 2005 to SPARK 2014. SPARK 2005 Features and SPARK 2014 Alternatives ----------------------------------------------- Nearly every SPARK 2005 feature has a SPARK 2014 equivalent or there is an alternative way of providing the same feature in SPARK 2014. The only SPARK 2005 (not including RavenSPARK) features that do not have a direct alternative are: * the 'Always_Valid attribute; * the ability to add pre and postconditions to an instantiation of a generic subprogram, e.g., Unchecked_Conversion; and * a precondition on the body of a subprogram refining the one on the specification - this is not usually required in SPARK 2014, it is normally replaced by the use of expression functions. At the moment the first two features have to be accomplished using pragma Assume. The following subsections of this appendix demonstrate how many SPARK 2005 idioms map into SPARK 2014. As a quick reference the table below shows, for each SPARK 2005 annotation or SPARK 2005 specific feature, a reference to the equivalent or alternative in SPARK 2014. In the table headings 2014 RM is the SPARK Reference Manual and Mapping is this appendix, the SPARK 2005 to SPARK 2014 mapping specification. ================= ======================================== ========================================================= ======== SPARK 2005 SPARK 2014 2014 RM Mapping ================= ======================================== ========================================================= ======== ~ in post 'Old attribute - see Ada RM 6.1.1 :ref:`A.2.2 ` ~ in body 'Loop_Entry attribute :ref:`5.5.3 ` :ref:`A.7 ` <-> = A -> B (if A then B) - see Ada RM 4.5.7 :ref:`A.2.2 ` % not needed :ref:`A.7 ` always_valid not supported :ref:`A.4.1 ` assert pragma Assert_And_Cut :ref:`5.9 ` :ref:`A.4.2 ` assert in loop pragma Loop_Invariant :ref:`5.5.3 ` :ref:`A.4.1 ` assume pragma Assume :ref:`5.9 ` :ref:`A.4.1 ` check pragma Assert - see Ada RM 11.4.2 :ref:`A.4.1 ` derives on spec Depends aspect :ref:`6.1.5 ` :ref:`A.2.1 ` derives on body No separate spec - Depends aspect derives on body Separate spec - Refined_Depends aspect :ref:`7.2.5 ` :ref:`A.3.2 ` for all quantified_expression - see Ada RM 4.5.8 :ref:`A.2.3 ` for some quantified_expression - See Ada RM 4.5.8 :ref:`A.4.1 ` global on spec Global aspect :ref:`6.1.4 ` :ref:`A.2.1 ` global on body No separate spec - Global aspect global on body Separate spec - Refined_Global aspect :ref:`7.2.4 ` :ref:`A.2.4 ` hide pragma SPARK_Mode - see User Guide inherit not needed :ref:`A.3.4 ` initializes Initializes aspect :ref:`7.1.5 ` :ref:`A.2.4 ` main_program not needed object assertions rule declarations are not needed :ref:`A.5.3 ` own on spec Abstract_State aspect :ref:`7.1.4 ` :ref:`A.3.2 ` own on body Refined_State aspect :ref:`7.2.2 ` :ref:`A.3.2 ` post on spec postcondition - see Ada RM 6.1.1 :ref:`6.1.1 ` :ref:`A.2.2 ` post on body No separate spec - postcondition post on body Separate spec - Refined_Post aspect :ref:`7.2.7 ` pre precondition - see Ada RM 6.1.1 :ref:`6.1.1 ` proof functions Ghost functions :ref:`6.9 ` :ref:`A.5.3 ` proof types Ada types :ref:`A.5.5 ` return 'Result attribute - see Ada RM 6.1.1 :ref:`A.2.2 ` update delta aggregate :ref:`A.6 ` ================= ======================================== ========================================================= ======== Subprogram patterns ------------------- .. _ms-global_derives-label: Global and Derives ~~~~~~~~~~~~~~~~~~ This example demonstrates how global variables can be accessed through procedures/functions and presents how the SPARK 2005 `derives` annotation maps over to `depends` in SPARK 2014. The example consists of one procedure (`Swap`) and one function (`Add`). `Swap` accesses two global variables and swaps their contents while `Add` returns their sum. Specification in SPARK 2005: .. literalinclude:: ../code/global_derives/05/swap_add_05.ads :language: ada :linenos: body in SPARK 2005: .. literalinclude:: ../code/global_derives/05/swap_add_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__global_derives/swap_add_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__global_derives/swap_add_14.adb :language: ada :linenos: .. _ms-pre_post_return-label: Pre/Post/Return contracts ~~~~~~~~~~~~~~~~~~~~~~~~~ This example demonstrates how the `Pre`/`Post`/`Return` contracts are restructured and how they map from SPARK 2005 to SPARK 2014. Procedure `Swap` and function `Add` perform the same task as in the previous example, but the global variables have been replaced by parameters (this is not necessarry for proof) and they have been augmented by pre and post annotations. Two additional functions (`Max` and `Divide`) and one additional procedure (`Swap_Array_Elements`) have also been included in this example in order to demonstrate further features. `Max` returns the maximum of the two parameters. `Divide` returns the division of the two parameters after having ensured that the divisor is not equal to zero. The `Swap_Array_Elements` procedure swaps the contents of two elements of an array. Specification in SPARK 2005: .. literalinclude:: ../code/pre_post_return/05/swap_add_max_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/pre_post_return/05/swap_add_max_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__pre_post_return/swap_add_max_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__pre_post_return/swap_add_max_14.adb :language: ada :linenos: .. _ms-attributes_of_unconstrained_out_parameter_in_precondition-label: Attributes of unconstrained out parameter in precondition ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The following example illustrates the fact that the attributes of an unconstrained formal array parameter of mode "out" are permitted to appear in a precondition. The flow analyzer also needs to be smart about this, since it knows that X'First and X'Last are well-defined in the body, even though the content of X is not. Specification in SPARK 2005: .. literalinclude:: ../code/attributes_of_unconstrained_out_parameter_in_precondition/05/p.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/attributes_of_unconstrained_out_parameter_in_precondition/05/p.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__attributes_of_unconstrained_out_parameter_in_precondition/p.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__attributes_of_unconstrained_out_parameter_in_precondition/p.adb :language: ada :linenos: .. _ms-nesting_refinement-label: Data Abstraction, Refinement and Initialization ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This example demonstrates data abstraction and refinement. It also shows how abstract data is shown to be initialized during package elaboration (it need not be - it could be initialized through an explicit subprogram call, in which case the Initalizes annotation should not be given). There is also a demonstration of how procedures and functions can be nested within other procedures and functions. Furthermore, it illustrates how global variable refinement can be performed. Specification in SPARK 2005: .. literalinclude:: ../code/nesting_refinement/05/nesting_refinement_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/nesting_refinement/05/nesting_refinement_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__nesting_refinement/nesting_refinement_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__nesting_refinement/nesting_refinement_14.adb :language: ada :linenos: Package patterns ---------------- Abstract Data Types (ADTs) ~~~~~~~~~~~~~~~~~~~~~~~~~~ .. _ms-adt_visible-label: Visible type ^^^^^^^^^^^^ The following example adds no mapping information. The SPARK 2005 and SPARK 2014 versions of the code are identical. Only the specification of the SPARK 2005 code will be presented. The reason why this code is being provided is to allow for a comparison between a package that is purely public and an equivalent one that also has private elements. Specification in SPARK 2005: .. literalinclude:: ../code/adt_visible/05/stacks_05.ads :language: ada :linenos: .. _ms-adt_private-label: Private type ^^^^^^^^^^^^ Similarly to the previous example, this one does not contain any annotations either. Due to this, the SPARK 2005 and SPARK 2014 versions are exactly the same. Only the specification of the 2005 version shall be presented. Specification in SPARK 2005: .. literalinclude:: ../code/adt_private/05/stacks_05.ads :language: ada :linenos: .. _ms-adt_private_refinement-label: Private type with pre/post contracts ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This example demonstrates how `pre` and `post` conditions of subprograms may be specified in terms of functions declared in the same package specification. The function declarations are completed in the body and the postconditions of the completed functions are used to prove the implementations of the other subprograms. In SPARK 2014 explicit postconditions do not have to be specified on the bodies of the functions as they are implemented as expression functions and the expression, E, of the function acts as a default refined postcondition, i.e., F'Result = E. Note that the SPARK 2014 version is proven entirely automatically whereas the SPARK 2005 version requires user defined proof rules. Specification in SPARK 2005: .. literalinclude:: ../code/adt_private_refinement/05/stacks_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/adt_private_refinement/05/stacks_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_refinement/stacks_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_refinement/stacks_14.adb :language: ada :linenos: .. _ms-adt_public_child_non_tagged_parent-label: .. Tagged types not supported as yet Public child extends non-tagged parent ADT ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example covers the main differences between a child package and an arbitrary package, namely: * The private part of a child package can access the private part of its parent. * The body of a child package can access the private part of its parent. * The child does not need a with clause for its parent. A private type and private constant are declared in the parent. The former is accessed in the body of the child, while the latter is accessed in the private part of the child. Specifications of both parent and child in SPARK 2005: .. literalinclude:: ../code/adt_public_child_non_tagged_parent/05/pairs_05.ads :language: ada :linenos: .. literalinclude:: ../code/adt_public_child_non_tagged_parent/05/pairs_05_additional_05.ads :language: ada :linenos: Bodies of both parent and child in SPARK 2005: .. literalinclude:: ../code/adt_public_child_non_tagged_parent/05/pairs_05.adb :language: ada :linenos: .. literalinclude:: ../code/adt_public_child_non_tagged_parent/05/pairs_05_additional_05.adb :language: ada :linenos: Specifications of both parent and child in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_public_child_non_tagged_parent/pairs_14.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_public_child_non_tagged_parent/pairs_14_additional_14.ads :language: ada :linenos: Bodies of both parent and child in SPARK 2014: As per SPARK 2005. .. _ms-adt_tagged_type-label: .. Tagged types not supported as yet Tagged type in root ADT package ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example illustrates the use of a tagged type in an ADT package. Specification in SPARK 2005: .. literalinclude:: ../code/adt_tagged_type/05/stacks_05.ads :language: ada :linenos: Body in SPARK 2005: N/A Specification in SPARK 2014: .. literalinclude:: ../code/adt_tagged_type/14/stacks_14.ads :language: ada :linenos: Body in SPARK 2014: N/A .. _ms-adt_tagged_type_extension-label: .. Tagged types not supported as yet Extension of tagged type in child package ADT ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example illustrates the extension of a tagged type in a child package. Specification in SPARK 2005: .. literalinclude:: ../code/adt_tagged_type_extension/05/stacks_05_monitored_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/adt_tagged_type_extension/05/stacks_05_monitored_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_tagged_type_extension/stacks_14_monitored_14.ads :language: ada :linenos: Body in SPARK 2014: As per SPARK 2005. .. _ms-adt_private_public_child_visibility-label: Private/Public child visibility ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example demonstrates visibility rules that apply between public children, private children and their parent in SPARK 2005. More specifically, it shows that: * Private children are able to see their private siblings but not their public siblings. * Public children are able to see their public siblings but not their private siblings. * All children have access to their parent but the parent can only access private children. Applying the SPARK tools on the following files will produce certain errors. This was intentionally done in order to illustrate both legal and illegal access attempts. SPARK 2014 shares Ada's visibility rules. No restrictions have been applied in terms of visibility. Note that SPARK 2014 code does not require Inherit annotations. Specification of parent in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05.ads :language: ada :linenos: Specification of private child A in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05-private_child_a_05.ads :language: ada :linenos: Specification of private child B in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05-private_child_b_05.ads :language: ada :linenos: Specification of public child A in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05-public_child_a_05.ads :language: ada :linenos: Specification of public child B in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05-public_child_b_05.ads :language: ada :linenos: Body of parent in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05.adb :language: ada :linenos: Body of public child A in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05-public_child_a_05.adb :language: ada :linenos: Body of public child B in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05-public_child_b_05.adb :language: ada :linenos: Body of private child B in SPARK 2005: .. literalinclude:: ../code/adt_private_public_child_visibility/05/parent_05-private_child_b_05.adb :language: ada :linenos: Specification of parent in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14.ads :language: ada :linenos: Specification of private child A in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14-private_child_a_14.ads :language: ada :linenos: Specification of private child B in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14-private_child_b_14.ads :language: ada :linenos: Specification of public child A in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14-public_child_a_14.ads :language: ada :linenos: Specification of public child B in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14-public_child_b_14.ads :language: ada :linenos: Body of parent in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14.adb :language: ada :linenos: Body of public child A in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14-public_child_a_14.adb :language: ada :linenos: Body of public child B in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14-public_child_b_14.adb :language: ada :linenos: Body of private child B in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__adt_private_public_child_visibility/parent_14-private_child_b_14.adb :language: ada :linenos: .. _ms-asm-label: Abstract State Machines (ASMs) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Visible, concrete state ^^^^^^^^^^^^^^^^^^^^^^^ .. _ms-asm_visible_concrete_initialized_by_declaration-label: Initialized by declaration ++++++++++++++++++++++++++ The example that follows presents a way in SPARK 2005 of initializing a concrete own variable (a state that is not refined) at the point of the declaration of the variables that compose it. Generally it is not good practice to declare several concrete own variables, data abstraction should be used but here we are doing it for the point of illustration. In SPARK 2014 the client's view of package state is either visible (declared in the visible part of the package) or a state abstraction representing hidden state. A variable cannot overload the name of a state abstraction and therefore a state abstraction must be completed by a refinement given in the body of the package - there is no concept of a concrete state abstraction. The constituents of a state abstraction may be initialized at their declaration. Specification in SPARK 2005: .. literalinclude:: ../code/asm_visible_concrete_initialized_by_declaration/05/stack_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/asm_visible_concrete_initialized_by_declaration/05/stack_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_visible_concrete_initialized_by_declaration/stack_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_visible_concrete_initialized_by_declaration/stack_14.adb :language: ada :linenos: .. _ms-asm_visible_concrete_initialized_by_elaboration-label: Initialized by elaboration ++++++++++++++++++++++++++ The following example presents how a package's concrete state can be initialized at the statements section of the body. The specifications of both SPARK 2005 and SPARK 2014 are not presented since they are identical to the specifications of the previous example. Body in SPARK 2005: .. literalinclude:: ../code/asm_visible_concrete_initialized_by_elaboration/05/stack_05.adb :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_visible_concrete_initialized_by_elaboration/stack_14.adb :language: ada :linenos: .. _ms-asm_private_concrete-label: Private, concrete state ^^^^^^^^^^^^^^^^^^^^^^^ In SPARK 2005 variables declared in the private part of a package are considered to be concrete own variables. In SPARK 2014 they are hidden state and must be constituents of a state abstraction. The SPARK 2005 body has not been included since it does not contain any annotations. Specification in SPARK 2005: .. literalinclude:: ../code/asm_private_concrete/05/stack_05.ads :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_concrete/stack_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_concrete/stack_14.adb :language: ada :linenos: Private, abstract state, refining onto concrete states in body ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ .. _ms-asm_private_abstract_bodyref_procedureinit-label: Initialized by procedure call +++++++++++++++++++++++++++++ In this example, the abstract state declared at the specification is refined at the body. Procedure `Init` can be invoked by users of the package, in order to initialize the state. Specification in SPARK 2005: .. literalinclude:: ../code/asm_private_abstract_bodyref_procedureinit/05/stack_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/asm_private_abstract_bodyref_procedureinit/05/stack_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_abstract_bodyref_procedureinit/stack_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_abstract_bodyref_procedureinit/stack_14.adb :language: ada :linenos: .. _ms-asm_private_abstract_bodyref_elaborationinit-label: Initialized by elaboration of declaration +++++++++++++++++++++++++++++++++++++++++ The example that follows introduces an abstract state at the specification and refines it at the body. The constituents of the abstract state are initialized at declaration. Specification in SPARK 2005: .. literalinclude:: ../code/asm_private_abstract_bodyref_elaborationinit/05/stack_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/asm_private_abstract_bodyref_elaborationinit/05/stack_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_abstract_bodyref_elaborationinit/stack_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_abstract_bodyref_elaborationinit/stack_14.adb :language: ada :linenos: .. _ms-asm_private_abstract_bodyref_statementinit-label: Initialized by package body statements ++++++++++++++++++++++++++++++++++++++ This example introduces an abstract state at the specification and refines it at the body. The constituents of the abstract state are initialized at the statements part of the body. The specifications of the SPARK 2005 and SPARK 2014 versions of the code are as in the previous example and have thus not been included. Body in SPARK 2005: .. literalinclude:: ../code/asm_private_abstract_bodyref_statementinit/05/stack_05.adb :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_abstract_bodyref_statementinit/stack_14.adb :language: ada :linenos: .. _ms-asm_private_abstract_bodyref_mixedinit-label: Initialized by mixture of declaration and statements ++++++++++++++++++++++++++++++++++++++++++++++++++++ This example introduces an abstract state at the specification and refines it at the body. Some of the constituents of the abstract state are initialized during their declaration and the rest at the statements part of the body. Specification in SPARK 2005: .. literalinclude:: ../code/asm_private_abstract_bodyref_mixedinit/05/stack_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/asm_private_abstract_bodyref_mixedinit/05/stack_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_abstract_bodyref_mixedinit/stack_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_private_abstract_bodyref_mixedinit/stack_14.adb :language: ada :linenos: .. _ms-asm_initial_condition-label: Initial condition ^^^^^^^^^^^^^^^^^ This example introduces a new SPARK 2014 feature that did not exist in SPARK 2005. On top of declaring an abstract state and promising to initialize it, we also illustrate certain conditions that will be valid after initialization. There is a verification condition to show that immediately after the elaboration of the package that the specified Initial_Condition is True. Checks will be generated that have to be proven (or executed at run-time) to show that the initial condition is True. Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_initial_condition/stack_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_initial_condition/stack_14.adb :language: ada :linenos: .. _ms-asm_abstract_state_refined_in_private_child-label: Private, abstract state, refining onto state of private child ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example shows a parent package Power that contains an own variable (a state abstraction). This state abstraction is refined onto state abstractions of two private children Source_A and Source_B. Specification of Parent in SPARK 2005: .. literalinclude:: ../code/asm_abstract_state_refined_in_private_child/05/power_05.ads :language: ada :linenos: Body of Parent in SPARK 2005: .. literalinclude:: ../code/asm_abstract_state_refined_in_private_child/05/power_05.adb :language: ada :linenos: Specifications of Private Children in SPARK 2005: .. literalinclude:: ../code/asm_abstract_state_refined_in_private_child/05/power_05_source_a_05.ads :language: ada :linenos: .. literalinclude:: ../code/asm_abstract_state_refined_in_private_child/05/power_05_source_b_05.ads :language: ada :linenos: Bodies of Private Children in SPARK 2005: .. literalinclude:: ../code/asm_abstract_state_refined_in_private_child/05/power_05_source_a_05.adb :language: ada :linenos: .. literalinclude:: ../code/asm_abstract_state_refined_in_private_child/05/power_05_source_b_05.adb :language: ada :linenos: Specification of Parent in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_private_child/power_14.ads :language: ada :linenos: Body of Parent in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_private_child/power_14.adb :language: ada :linenos: Specifications of Private Children in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_private_child/power_14-source_a_14.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_private_child/power_14-source_b_14.ads :language: ada :linenos: Bodies of Private Children in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_private_child/power_14-source_a_14.adb :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_private_child/power_14-source_b_14.adb :language: ada :linenos: .. _ms-asm_abstract_state_refined_in_embedded_package-label: Private, abstract state, refining onto concrete state of embedded package ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This example is based around the packages from section :ref:`ms-asm_abstract_state_refined_in_embedded_package-label`, with the private child packages converted into embedded packages and the refinement onto concrete visible state. Specification in SPARK 2005: .. literalinclude:: ../code/asm_abstract_state_refined_in_embedded_package/05/power_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/asm_abstract_state_refined_in_embedded_package/05/power_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_embedded_package/power_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__asm_abstract_state_refined_in_embedded_package/power_14.adb :language: ada :linenos: .. _ms-asm_abstract_state_refined_in_embedded_and_private_child-label: Private, abstract state, refining onto mixture of the above ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This example is based around the packages from sections :ref:`ms-asm_abstract_state_refined_in_private_child-label` and :ref:`ms-asm_abstract_state_refined_in_embedded_package-label`. Source_A is an embedded package, while Source_B is a private child. In order to avoid repetition, the code of this example is not being presented. External Variables ~~~~~~~~~~~~~~~~~~ .. _ms-external_variables_input_output-label: Basic Input and Output Device Drivers ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example shows a main program - Copy - that reads all available data from a given input port, stores it internally during the reading process in a stack and then outputs all the data read to an output port. The specifications of the stack packages are not presented since they are identical to previous examples. Specification of main program in SPARK 2005: .. literalinclude:: ../code/external_variables_input_output/05/copy_05.adb :language: ada :linenos: Specification of input port in SPARK 2005: .. literalinclude:: ../code/external_variables_input_output/05/input_port_05.ads :language: ada :linenos: Body of input port in SPARK 2005: .. literalinclude:: ../code/external_variables_input_output/05/input_port_05.adb :language: ada :linenos: Specification of output port in SPARK 2005: .. literalinclude:: ../code/external_variables_input_output/05/output_port_05.ads :language: ada :linenos: Body of output port in SPARK 2005: .. literalinclude:: ../code/external_variables_input_output/05/output_port_05.adb :language: ada :linenos: Specification of main program in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_input_output/copy_14.adb :language: ada :linenos: Specification of input port in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_input_output/input_port_14.ads :language: ada :linenos: Specification of output port in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_input_output/output_port_14.ads :language: ada :linenos: Body of input port in SPARK 2014: This is as per SPARK 2005, but uses aspects instead of representation clauses and pragmas. .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_input_output/input_port_14.adb :language: ada :linenos: Body of output port in SPARK 2014: This is as per SPARK 2005, but uses aspects instead of representation clauses and pragmas. .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_input_output/output_port_14.adb :language: ada :linenos: .. _ms-external_variables_input_append_tail-label: Input driver using \'Tail in a contract ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This example uses the Input_Port package from section `Basic Input and Output Device Drivers`_ and adds a contract using the 'Tail attribute. The example also use the Always_Valid attribute in order to allow proof to succeed (otherwise, there is no guarantee in the proof context that the value read from the port is of the correct type). SPARK 2014 does not have the attribute 'Tail but, often, an equivalent proof can be achieved using assert pragmas. Neither is there a direct equivalent of the Always_Valid attribute but the paragma Assume may be used to the same effect. Specification in SPARK 2005: .. literalinclude:: ../code/external_variables_input_append_tail/05/input_port_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/external_variables_input_append_tail/05/input_port_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_input_append_tail/input_port_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_input_append_tail/input_port_14.adb :language: ada :linenos: .. _ms-external_variables_output_append_tail-label: Output driver using \'Append in a contract ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This example uses the Output package from section `Basic Input and Output Device Drivers`_ and adds a contract using the 'Append attribute. SPARK 2014 does not have the attribute 'Append but, often, an equivalent proof can be achieved using assert pragmas. Specification in SPARK 2005: .. literalinclude:: ../code/external_variables_output_append_tail/05/output_port_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/external_variables_output_append_tail/05/output_port_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_output_append_tail/output_port_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_output_append_tail/output_port_14.adb :language: ada :linenos: .. _ms-external_variables_refinement_voting_input_switch-label: Refinement of external state - voting input switch ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example presents an abstract view of the reading of 3 individual switches and the voting performed on the values read. Abstract Switch specification in SPARK 2005: .. literalinclude:: ../code/external_variables_refinement_voting_input_switch/05/switch.ads :language: ada :linenos: Component Switch specifications in SPARK 2005: .. literalinclude:: ../code/external_variables_refinement_voting_input_switch/05/switch-val1.ads :language: ada :linenos: .. literalinclude:: ../code/external_variables_refinement_voting_input_switch/05/switch-val2.ads :language: ada :linenos: .. literalinclude:: ../code/external_variables_refinement_voting_input_switch/05/switch-val3.ads :language: ada :linenos: Switch body in SPARK 2005: .. literalinclude:: ../code/external_variables_refinement_voting_input_switch/05/switch.adb :language: ada :linenos: Abstract Switch specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_refinement_voting_input_switch/switch.ads :language: ada :linenos: Component Switch specifications in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_refinement_voting_input_switch/switch-val1.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_refinement_voting_input_switch/switch-val2.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_refinement_voting_input_switch/switch-val3.ads :language: ada :linenos: Switch body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_refinement_voting_input_switch/switch.adb :language: ada :linenos: .. _ms-external_variables_complex_io_device-label: Complex I/O Device ^^^^^^^^^^^^^^^^^^ The following example illustrates a more complex I/O device: the device is fundamentally an output device but an acknowledgement has to be read from it. In addition, a local register stores the last value written to avoid writes that would just re-send the same value. The own variable is then refined into a normal variable, an input external variable and an output external variable. Specification in SPARK 2005: .. literalinclude:: ../code/external_variables_complex_io_device/05/device.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/external_variables_complex_io_device/05/device.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_complex_io_device/device.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_complex_io_device/device.adb :language: ada :linenos: .. _ms-external_variables_increasing_values_in_input_stream-label: Increasing values in input stream ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example illustrates an input port from which values are read. According to its postcondition, procedure Increases checks whether the first values read from the sequence are in ascending order. This example shows that postconditions can refer to multiple individual elements of the input stream. In SPARK 2014 we can use assert pragmas in the subprogram instead of specifying the action in the postcondition, as was done in :ref:`ms-external_variables_input_append_tail-label`. Another alternative, as shown in this example, is to use a formal parameter of a private type to keep a trace of the values read. Specification in SPARK 2005: .. literalinclude:: ../code/external_variables_increasing_values_in_input_stream/05/inc.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/external_variables_increasing_values_in_input_stream/05/inc.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_increasing_values_in_input_stream/inc.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__external_variables_increasing_values_in_input_stream/inc.adb :language: ada :linenos: .. _ms-package_inheritance-label: Package Inheritance ~~~~~~~~~~~~~~~~~~~ SPARK 2014 does not have the SPARK 2005 concept of package inheritance. It has the same package visibility rules as Ada. .. _ms-contracts_with_remote_state-label: Contracts with remote state ^^^^^^^^^^^^^^^^^^^^^^^^^^^ The following example illustrates indirect access to the state of one package by another via an intermediary. Raw_Data stores some data, which has preprocessing performed on it by Processing and on which Calculate performs some further processing (although the corresponding bodies are not given, Read_Calculated_Value in Calculate calls through to Read_Processed_Data in Processing, which calls through to Read in Raw_Data). Specifications in SPARK 2005: .. literalinclude:: ../code/contracts_with_remote_state/05/raw_data.ads :language: ada :linenos: .. literalinclude:: ../code/contracts_with_remote_state/05/processing.ads :language: ada :linenos: .. literalinclude:: ../code/contracts_with_remote_state/05/calculate.ads :language: ada :linenos: Specifications in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__contracts_with_remote_state/raw_data.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__contracts_with_remote_state/processing.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__contracts_with_remote_state/calculate.ads :language: ada :linenos: .. _ms-package_nested_inside_package-label: Package nested inside package ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ See section `Private, abstract state, refining onto concrete state of embedded package`_. .. _ms-package_nested_inside_subprogram-label: Package nested inside subprogram ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This example is a modified version of that given in section `Refinement of external state - voting input switch`_. It illustrates the use of a package nested within a subprogram. Abstract Switch specification in SPARK 2005: .. literalinclude:: ../code/package_nested_inside_subprogram/05/switch.ads :language: ada :linenos: Component Switch specifications in SPARK 2005: As in `Refinement of external state - voting input switch`_ Switch body in SPARK 2005: .. literalinclude:: ../code/package_nested_inside_subprogram/05/switch.adb :language: ada :linenos: Abstract Switch specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__package_nested_inside_subprogram/switch.ads :language: ada :linenos: Component Switch specification in SPARK 2014: As in `Refinement of external state - voting input switch`_ Switch body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__package_nested_inside_subprogram/switch.adb :language: ada :linenos: .. _ms-circular_dependence_and_elaboration_order-label: Circular dependence and elaboration order ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ SPARK 2005 avoided issues of circular dependence and elaboration order dependencies through a combination of the inherit annotation and the restrictions that initialization expressions are constant, user defined subprograms cannot be called in the sequence of statements of a package body and a package can only initialize variables declared in its delarative part. SPARK 2014 does not have the inherit annotation and only enforces the restriction that a package can only initialize an object declared in its declarative region. Hence, in SPARK 2014 two package bodies that depend on each other's specification may be legal, as is calling a user defined subprogram. Instead of the elaboration restrictions of SPARK 2005 a set of rules is applied in SPARK 2014 which determines when elaboration order control pragmas such as Elaborate_Body or Elaborate_All are required. These rules ensure the absence of elaboration order dependencies. Examples of the features of SPARK 2014 elaboration order rules are given below. In the example described below the partial elaboration order would be either of P_14 or Q_14 specifications first followed by P_14 body because of the Elaborate_All on the specification of R_14 specification and the body of Q_14, then the elaboration of Q_14 body or the specification of R_14 and the body of R_14 after the elaboration of Q_14. Elaboration order dependencies are avoided by the (required) use of elaboration control pragmas. Package Specifications in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__circular_dependence_and_elaboration_order/p_14.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__circular_dependence_and_elaboration_order/q_14.ads :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__circular_dependence_and_elaboration_order/r_14.ads :language: ada :linenos: Package Bodies in SPARK 2014 .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__circular_dependence_and_elaboration_order/p_14.adb :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__circular_dependence_and_elaboration_order/q_14.adb :language: ada :linenos: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__circular_dependence_and_elaboration_order/r_14.adb :language: ada :linenos: Bodies and Proof ---------------- Assert, Assume, Check contracts ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. _ms-assert_loop_contract-label: Assert (in loop) contract ^^^^^^^^^^^^^^^^^^^^^^^^^ The following example demonstrates how the SPARK 2005 `assert` annotation is used inside a loop as a loop invariant. It cuts the loop and on each iteration of the loop the list of existing hypotheses for the path is cleared. A verification condition is generated to prove that the assert expression is True, and the expression is the basis of the new hypotheses. SPARK 2014 has a specific pragma for defining a loop invariant, `pragma Loop_Invariant` which is more sophisticated than the SPARK 2005 assert annotation and often requires less conditions in the invariant expression than in SPARK 2005. As in SPARK 2005 a default loop invariant will be used if one is not provided which, often, may be sufficient to prove absence of run-time exceptions. Like all SPARK 2014 assertion expressions the loop invariant is executable. Note in the example below the SPARK 2014 version proves absence of run-time exceptions without an explicit loop invariant being provided. Specification in SPARK 2005: .. literalinclude:: ../code/assert_loop_contract/05/assert_loop_05.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/assert_loop_contract/05/assert_loop_05.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__assert_loop_contract/assert_loop_14.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__assert_loop_contract/assert_loop_14.adb :language: ada :linenos: .. _ms-assert_no_loop_contract-label: Assert (no loop) contract ^^^^^^^^^^^^^^^^^^^^^^^^^ While not in a loop, the SPARK 2005 `assert` annotation maps to `pragma Assert_And_Cut` in SPARK 2014. Both the assert annotation and pragma assert clear the list of hypotheses on the path, generate a verification condition to prove the assertion expression and use the assertion expression as the basis of the new hypotheses. .. _ms-proof_assume_contract-label: Assume contract ^^^^^^^^^^^^^^^ The following example illustrates use of an Assume annotation. The assumed expression does not generate a verification condition and is not proved (although it is executed in SPARK 2014 if assertion expressions are not ignored at run-time). In this example, the Assume annotation is effectively being used to implement the SPARK 2005 Always_Valid attribute. Specification for Assume annotation in SPARK 2005: .. literalinclude:: ../code/proof_assume_contract/05/input_port.ads :language: ada :linenos: Body for Assume annotation in SPARK 2005: .. literalinclude:: ../code/proof_assume_contract/05/input_port.adb :language: ada :linenos: Specification for Assume annotation in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__proof_assume_contract/input_port.ads :language: ada :linenos: Body for Assume annotation in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__proof_assume_contract/input_port.adb :language: ada :linenos: .. _ms-check_contract-label: Check contract ^^^^^^^^^^^^^^ The SPARK 2005 `check` annotation is replaced by `pragma assert` in SPARK 2014. This annotation generates a verification condition to prove the checked expression and adds the expression as a new hypothesis to the list of existing hypotheses. Specification for Check annotation in SPARK 2005: .. literalinclude:: ../code/check_contract/05/check_05.ads :language: ada :linenos: Body for Check annotation in SPARK 2005: .. literalinclude:: ../code/check_contract/05/check_05.adb :language: ada :linenos: Specification for Check annotation in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__check_contract/check_14.ads :language: ada :linenos: Body for Check annotation in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__check_contract/check_14.adb :language: ada :linenos: Assert used to control path explosion ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This capability is in general not needed with the SPARK 2014 toolset where path explosion is handled automatically. In the rare cases where this is needed you can use `pragma Assert_And_Cut`. Other Contracts and Annotations ------------------------------- Always_Valid assertion ~~~~~~~~~~~~~~~~~~~~~~ See section `Input driver using \'Tail in a contract`_ for use of an assertion involving the Always_Valid attribute. Rule declaration annotation ~~~~~~~~~~~~~~~~~~~~~~~~~~~ See section `Proof types and proof functions`_. .. _ms-proof_types_and_proof_functions-label: Proof types and proof functions ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The following example gives pre- and postconditions on operations that act upon the concrete representation of an abstract own variable. This means that proof functions and proof types are needed to state those pre- and postconditions. In addition, it gives an example of the use of a rule declaration annotation - in the body of procedure Initialize - to introduce a rule related to the components of a constant record value. SPARK 2014 does not have a direct equivalent of proof types and proof functions. State abstractions cannot have a type and all functions in SPARK 2014 are Ada functions. Functions may be defined to be ghost functions which means that they can only be called within an assertion expression such as a pre or postcondition. Assertion expressions may be executed or ignored at run-time and if they are ignored Ghost functions behave much like SPARK 2005 proof functions. Rule declaration annotations for structured constants are not required in SPARK 2014. The SPARK 2005 version of the example given below will require user defined proof rules to discharge the proofs because refined definitions of some of the proof functions cannot be provided as they would have different formal parameters. The SPARK 2014 version does not suffer from this problem as functions called within assertion expressions may have global items. Specification in SPARK 2005: .. literalinclude:: ../code/other_proof_types_and_functions/05/stack.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/other_proof_types_and_functions/05/stack.adb :language: ada :linenos: Specification in SPARK 2014 .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__other_proof_types_and_functions/stack.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__other_proof_types_and_functions/stack.adb :language: ada :linenos: Using an External Prover ~~~~~~~~~~~~~~~~~~~~~~~~ One may wish to use an external prover such as Isabelle, with rules defining a ghost function written in the prover input language. This can be done in SPARK 2014 by denoting the ghost function as an Import in lieu of providing a body for it. Of course such ghost functions cannot be executed. Specification in SPARK 2014 using an external prover: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__other_proof_types_and_functions/stack_external_prover.ads :language: ada :linenos: .. _ms-quote_own_variable_in_contract-label: Quoting an Own Variable in a Contract ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Sometimes it is necessary to reference an own variable (a state abstraction) in a contract. In SPARK 2005 this was achieved by declaring the own variable with a type, either concrete or abstract. As seen in :ref:`ms-proof_types_and_proof_functions-label`. Once the own variable has a type it can be used in a SPARK 2005 proof context. A state abstraction in SPARK 2014 does not have a type. Instead, an Ada type to represent the abstract state is declared. A function which has the state abstraction as a global item is then declared which returns an object of the type. This function may have the same name as the state abstraction (the name is overloaded). References which appear to be the abstract state in an assertion expression are in fact calls to the overloaded function. An example of this technique is given in the following example which is a version of the stack example given in :ref:`ms-proof_types_and_proof_functions-label` but with the post conditions extended to express the functional properties of the stack. The extension requires the quoting of the own variable/state abstraction in the postcondition in order to state that the contents of the stack other than the top entries are not changed. Specification in SPARK 2005: .. literalinclude:: ../code/other_proof_types_and_functions/05/stack_functional_spec.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/other_proof_types_and_functions/05/stack_functional_spec.adb :language: ada :linenos: Specification in SPARK 2014 .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__other_proof_types_and_functions/stack_functional_spec.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__other_proof_types_and_functions/stack_functional_spec.adb :language: ada :linenos: Main_Program annotation ~~~~~~~~~~~~~~~~~~~~~~~ This annotation isn't needed. Currently any parameterless procedure declared at library-level is considered as a potential main program and analyzed as such. .. _ms-update_expressions-label: Update Expressions ------------------ SPARK 2005 has update expressions for updating records and arrays. They can only be used in SPARK 2005 proof contexts. The equivalent in SPARK 2014 is a delta aggregate. This can be used in any Ada expression. Specification in SPARK 2005: .. literalinclude:: ../code/update_examples/05/update_examples.ads :language: ada :linenos: Specification in SPARK 2014 .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_Examples/update_examples.ads :language: ada :linenos: .. _ms-value_of_variable_on_entry_to_a_loop-label: Value of Variable on Entry to a Loop ------------------------------------ In SPARK 2005 the entry value of a for loop variable variable, X, can be referenced using the notation X%. This notation is required frequently when the variable is referenced in a proof context within the loop. Often it is needed to state that the value of X is not changed within the loop by stating X = X%. This notation is restricted to a variable which defines the lower or upper range of a for loop. SPARK 2014 has a more general scheme whereby the loop entry value of any variable can be denoted within any sort of loop using the '*Loop_Entry* attribute. However, its main use is not for showing that the value of a for loop variable has not changed as the SPARK 2014 tools are able to determine this automatically. Rather it is used instead of ~ in loops because the attribute 'Old is only permitted in postconditions (including Contract_Cases). Specification in SPARK 2005: .. literalinclude:: ../code/loop_entry/05/loop_entry.ads :language: ada :linenos: Body in SPARK 2005: .. literalinclude:: ../code/loop_entry/05/loop_entry.adb :language: ada :linenos: Specification in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__loop_entry/loop_entry.ads :language: ada :linenos: Body in SPARK 2014: .. literalinclude:: ../../../testsuite/gnatprove/tests/RM_MS__loop_entry/loop_entry.adb :language: ada :linenos: .. RavenSPARK patterns ~~~~~~~~~~~~~~~~~~~ The Ravenscar profile for tasking is not yet supported in SPARK 2014. Mapping examples will be added here in future.