# 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

A.2.2

~ in body

‘Loop_Entry attribute

5.5.3

A.7

<->

=

A -> B

(if A then B) - see Ada RM 4.5.7

A.2.2

%

not needed

A.7

always_valid

not supported

A.4.1

assert

pragma Assert_And_Cut

5.9

A.4.2

assert in loop

pragma Loop_Invariant

5.5.3

A.4.1

assume

pragma Assume

5.9

A.4.1

check

pragma Assert - see Ada RM 11.4.2

A.4.1

derives on spec

Depends aspect

6.1.5

A.2.1

derives on body

No separate spec - Depends aspect

derives on body

Separate spec - Refined_Depends aspect

7.2.5

A.3.2

for all

quantified_expression - see Ada RM 4.5.8

A.2.3

for some

quantified_expression - See Ada RM 4.5.8

A.4.1

global on spec

Global aspect

6.1.4

A.2.1

global on body

No separate spec - Global aspect

global on body

Separate spec - Refined_Global aspect

7.2.4

A.2.4

hide

pragma SPARK_Mode - see User Guide

inherit

not needed

A.3.4

initializes

Initializes aspect

7.1.5

A.2.4

main_program

not needed

object assertions

rule declarations are not needed

A.5.3

own on spec

Abstract_State aspect

7.1.4

A.3.2

own on body

Refined_State aspect

7.2.2

A.3.2

post on spec

postcondition - see Ada RM 6.1.1

6.1.1

A.2.2

post on body

No separate spec - postcondition

post on body

Separate spec - Refined_Post aspect

7.2.7

pre

precondition - see Ada RM 6.1.1

6.1.1

proof functions

Ghost functions

6.9

A.5.3

proof types

A.5.5

return

‘Result attribute - see Ada RM 6.1.1

A.2.2

update

delta aggregate

A.6

## Subprogram patterns¶

### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 package Swap_Add_05 --# own X, Y: Integer; is X, Y: Integer; procedure Swap; --# global in out X, Y; --# derives X from Y & --# Y from X; function Add return Integer; --# global in X, Y; end Swap_Add_05; 

body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 package body Swap_Add_05 is procedure Swap is Temporary: Integer; begin Temporary := X; X := Y; Y := Temporary; end Swap; function Add return Integer is begin return X + Y; end Add; end Swap_Add_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 package Swap_Add_14 with SPARK_Mode is -- Visible variables are not state abstractions. X, Y: Integer; procedure Swap with Global => (In_Out => (X, Y)), Depends => (X => Y, -- to be read as "X depends on Y" Y => X); -- to be read as "Y depends on X" function Add return Integer with Global => (Input => (X, Y)); end Swap_Add_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package body Swap_Add_14 with SPARK_Mode is procedure Swap is Temporary: Integer; begin Temporary := X; X := Y; Y := Temporary; end Swap; function Add return Integer is (X + Y); end Swap_Add_14; 

### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 package Swap_Add_Max_05 is subtype Index is Integer range 1..100; type Array_Type is array (Index) of Integer; procedure Swap (X, Y : in out Integer); --# post X = Y~ and Y = X~; function Add (X, Y : Integer) return Integer; --# pre ((X >= 0 and Y >= 0) -> (X + Y <= Integer'Last)) and --# ((X < 0 and Y < 0) -> (X + Y >= Integer'First)); --# return X + Y; function Max (X, Y : Integer) return Integer; --# return Z => (X >= Y -> Z = X) and --# (Y > X -> Z = Y); function Divide (X, Y : Integer) return Integer; --# pre Y /= 0 and X > Integer'First; --# return X / Y; procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type); --# post A = A~[I => A~(J); J => A~(I)]; end Swap_Add_Max_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 package body Swap_Add_Max_05 is procedure Swap (X, Y: in out Integer) is Temporary: Integer; begin Temporary := X; X := Y; Y := Temporary; end Swap; function Add (X, Y : Integer) return Integer is begin return X + Y; end Add; function Max (X, Y : Integer) return Integer is Result: Integer; begin if X >= Y then Result := X; else Result := Y; end if; return Result; end Max; function Divide (X, Y : Integer) return Integer is begin return X / Y; end Divide; procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type) is Temporary: Integer; begin Temporary := A(I); A(I) := A(J); A(J) := Temporary; end Swap_Array_Elements; end Swap_Add_Max_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 package Swap_Add_Max_14 with SPARK_Mode is subtype Index is Integer range 1..100; type Array_Type is array (Index) of Integer; procedure Swap (X, Y : in out Integer) with Post => (X = Y'Old and Y = X'Old); function Add (X, Y : Integer) return Integer with Pre => (if X >= 0 and Y >= 0 then X <= Integer'Last - Y elsif X < 0 and Y < 0 then X >= Integer'First - Y), -- The precondition may be written as X + Y in Integer if -- an extended arithmetic mode is selected Post => Add'Result = X + Y; function Max (X, Y : Integer) return Integer with Post => Max'Result = (if X >= Y then X else Y); function Divide (X, Y : Integer) return Integer with Pre => Y /= 0 and X > Integer'First, Post => Divide'Result = X / Y; procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type) with Post => A = A'Old'Update (I => A'Old (J), J => A'Old (I)); end Swap_Add_Max_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 package body Swap_Add_Max_14 with SPARK_Mode is procedure Swap (X, Y : in out Integer) is Temporary: Integer; begin Temporary := X; X := Y; Y := Temporary; end Swap; function Add (X, Y : Integer) return Integer is (X + Y); function Max (X, Y : Integer) return Integer is (if X >= Y then X else Y); function Divide (X, Y : Integer) return Integer is (X / Y); procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type) is Temporary: Integer; begin Temporary := A(I); A(I) := A(J); A(J) := Temporary; end Swap_Array_Elements; end Swap_Add_Max_14; 

### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 package P is type A is array (Positive range <>) of Integer; -- Shows that X'First and X'Last _can_ be used in -- precondition here, even though X is mode "out"... procedure Init (X : out A); --# pre X'First = 1 and --# X'Last >= 20; --# post for all I in Positive range X'Range => --# ((I /= 20 -> (X (I) = 0)) and --# (I = 1 -> (X (I) = X'Last)) and --# (I = 20 -> (X (I) = -1))); end P; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 package body P is procedure Init (X : out A) is begin X := (others => 0); X (1) := X'Last; X (20) := -1; end Init; end P; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 package P with SPARK_Mode is type A is array (Positive range <>) of Integer; -- Shows that X'First, X'Last and X'Length _can_ be used -- in precondition here, even though X is mode "out"... procedure Init (X : out A) with Pre => X'First = 1 and X'Last >= 20, Post => (for all I in X'Range => (if I = 1 then X (I) = X'Last elsif I = 20 then X (I) = -1 else X (I) = 0)); end P; 

Body in SPARK 2014:

 1 2 3 4 5 6 7 8 package body P with SPARK_Mode is procedure Init (X : out A) is begin X := (1 => X'Last, 20 => -1, others => 0); end Init; end P; 

### 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:

 1 2 3 4 5 6 7 package Nesting_Refinement_05 --# own State; --# initializes State; is procedure Operate_On_State; --# global in out State; end Nesting_Refinement_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 package body Nesting_Refinement_05 --# own State is X, Y; -- Refined State is X, Y: Integer; procedure Operate_On_State --# global in out X; -- Refined Global --# out Y; is Z: Integer; procedure Add_Z_To_X --# global in out X; --# in Z; is begin X := X + Z; end Add_Z_To_X; procedure Overwrite_Y_With_Z --# global out Y; --# in Z; is begin Y := Z; end Overwrite_Y_With_Z; begin Z := 5; Add_Z_To_X; Overwrite_Y_With_Z; end Operate_On_State; begin -- Promised to initialize State -- (which consists of X and Y) X := 10; Y := 20; end Nesting_Refinement_05; 

Specification in SPARK 2014:

 1 2 3 4 5 6 7 8 package Nesting_Refinement_14 with SPARK_Mode, Abstract_State => State, Initializes => State is procedure Operate_On_State with Global => (In_Out => State); end Nesting_Refinement_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 package body Nesting_Refinement_14 -- State is refined onto two concrete variables X and Y with SPARK_Mode, Refined_State => (State => (X, Y)) is X, Y: Integer; procedure Operate_On_State with Refined_Global => (In_Out => X, Output => Y) is Z: Integer; procedure Add_Z_To_X with Global => (In_Out => X, Input => Z) is begin X := X + Z; end Add_Z_To_X; procedure Overwrite_Y_With_Z with Global => (Output => Y, Input => Z) is begin Y := Z; end Overwrite_Y_With_Z; begin Z := 5; Add_Z_To_X; Overwrite_Y_With_Z; end Operate_On_State; begin -- Promised to initialize State -- (which consists of X and Y) X := 10; Y := 20; end Nesting_Refinement_14; 

## Package patterns¶

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 package Stacks_05 is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1 .. Stack_Size; type Vector is array(Index_Range) of Integer; type Stack is record Stack_Vector : Vector; Stack_Pointer : Pointer_Range; end record; function Is_Empty(S : Stack) return Boolean; function Is_Full(S : Stack) return Boolean; procedure Clear(S : out Stack); procedure Push(S : in out Stack; X : in Integer); procedure Pop(S : in out Stack; X : out Integer); end Stacks_05; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 package Stacks_05 is type Stack is private; function Is_Empty(S : Stack) return Boolean; function Is_Full(S : Stack) return Boolean; procedure Clear(S : out Stack); procedure Push(S : in out Stack; X : in Integer); procedure Pop(S : in out Stack; X : out Integer); private Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1 .. Stack_Size; type Vector is array(Index_Range) of Integer; type Stack is record Stack_Vector : Vector; Stack_Pointer : Pointer_Range; end record; end Stacks_05; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 package Stacks_05 is type Stack is private; function Is_Empty(S : Stack) return Boolean; function Is_Full(S : Stack) return Boolean; procedure Clear(S : in out Stack); --# post Is_Empty(S); procedure Push(S : in out Stack; X : in Integer); --# pre not Is_Full(S); --# post not Is_Empty(S); procedure Pop(S : in out Stack; X : out Integer); --# pre not Is_Empty(S); --# post not Is_Full(S); private Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1 .. Stack_Size; type Vector is array(Index_Range) of Integer; type Stack is record Stack_Vector : Vector; Stack_Pointer : Pointer_Range; end record; end Stacks_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 package body Stacks_05 is function Is_Empty (S : Stack) return Boolean --# return S.Stack_Pointer = 0; is begin return S.Stack_Pointer = 0; end Is_Empty; function Is_Full (S : Stack) return Boolean --# return S.Stack_Pointer = Stack_Size; is begin return S.Stack_Pointer = Stack_Size; end Is_Full; procedure Clear (S : in out Stack) --# post Is_Empty(S); is begin S.Stack_Pointer := 0; end Clear; procedure Push (S : in out Stack; X : in Integer) is begin S.Stack_Pointer := S.Stack_Pointer + 1; S.Stack_Vector (S.Stack_Pointer) := X; end Push; procedure Pop (S : in out Stack; X : out Integer) is begin X := S.Stack_Vector (S.Stack_Pointer); S.Stack_Pointer := S.Stack_Pointer - 1; end Pop; end Stacks_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 package Stacks_14 with SPARK_Mode is type Stack is private; function Is_Empty(S : Stack) return Boolean; function Is_Full(S : Stack) return Boolean; procedure Clear(S : in out Stack) with Post => Is_Empty(S); procedure Push(S : in out Stack; X : in Integer) with Pre => not Is_Full(S), Post => not Is_Empty(S); procedure Pop(S : in out Stack; X : out Integer) with Pre => not Is_Empty(S), Post => not Is_Full(S); private Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1 .. Stack_Size; type Vector is array(Index_Range) of Integer; type Stack is record Stack_Vector : Vector; Stack_Pointer : Pointer_Range; end record; end Stacks_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 package body Stacks_14 with SPARK_Mode is -- Expression function has default refined postcondition of -- Is_Empty'Result = (S.Stack_Pointer = 0) function Is_Empty(S : Stack) return Boolean is (S.Stack_Pointer = 0); -- Expression function has default refined postcondition of -- Is_Empty'Result = (S.Stack_Pointer = Stack_Size) function Is_Full(S : Stack) return Boolean is (S.Stack_Pointer = Stack_Size); procedure Clear(S : in out Stack) is begin S.Stack_Pointer := 0; end Clear; procedure Push(S : in out Stack; X : in Integer) is begin S.Stack_Pointer := S.Stack_Pointer + 1; S.Stack_Vector(S.Stack_Pointer) := X; end Push; procedure Pop(S : in out Stack; X : out Integer) is begin X := S.Stack_Vector(S.Stack_Pointer); S.Stack_Pointer := S.Stack_Pointer - 1; end Pop; end Stacks_14; 

#### 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:

 1 2 3 4 5 package Parent_05 is function F (X : Integer) return Integer; function G (X : Integer) return Integer; end Parent_05; 

Specification of private child A in SPARK 2005:

 1 2 3 4 5 --#inherit Parent_05; -- OK private package Parent_05.Private_Child_A_05 is function F (X : Integer) return Integer; end Parent_05.Private_Child_A_05; 

Specification of private child B in SPARK 2005:

 1 2 3 4 5 6 --#inherit Parent_05.Private_Child_A_05, -- OK --# Parent_05.Public_Child_A_05; -- error, public sibling private package Parent_05.Private_Child_B_05 is function H (X : Integer) return Integer; end Parent_05.Private_Child_B_05; 

Specification of public child A in SPARK 2005:

 1 2 3 4 5 6 --#inherit Parent_05, -- OK --# Parent_05.Private_Child_A_05; -- error, private sibling package Parent_05.Public_Child_A_05 is function G (X : Integer) return Integer; end Parent_05.Public_Child_A_05; 

Specification of public child B in SPARK 2005:

 1 2 3 4 5 --#inherit Parent_05.Public_Child_A_05; -- OK package Parent_05.Public_Child_B_05 is function H (X : Integer) return Integer; end Parent_05.Public_Child_B_05; 

Body of parent in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 with Parent_05.Private_Child_A_05, -- OK Parent_05.Public_Child_A_05; -- error, public children not visible package body Parent_05 is function F (X : Integer) return Integer is begin return Private_Child_A_05.F (X); end F; function G (X : Integer) return Integer is begin return Public_Child_A_05.G (X); end G; end Parent_05; 

Body of public child A in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package body Parent_05.Public_Child_A_05 is function G (X : Integer) return Integer is Result : Integer; begin if X <= 0 then Result := 0; else Result := Parent_05.F (X); -- OK end if; return Result; end G; end Parent_05.Public_Child_A_05; 

Body of public child B in SPARK 2005:

 1 2 3 4 5 6 7 8 with Parent_05.Private_Child_B_05; package body Parent_05.Public_Child_B_05 is function H (X : Integer) return Integer is begin return Parent_05.Private_Child_B_05.H (X); end H; end Parent_05.Public_Child_B_05; 

Body of private child B in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package body Parent_05.Private_Child_B_05 is function H (X : Integer) return Integer is Result : Integer; begin if X <= 10 then Result := 10; else Result := Parent_05.F (X); -- Illegal in SPARK 2005 end if; return Result; end H; end Parent_05.Private_Child_B_05; 

Specification of parent in SPARK 2014:

 1 2 3 4 5 6 package Parent_14 with SPARK_Mode is function F (X : Integer) return Integer; function G (X : Integer) return Integer; end Parent_14; 

Specification of private child A in SPARK 2014:

 1 2 3 4 5 private package Parent_14.Private_Child_A_14 with SPARK_Mode is function F (X : Integer) return Integer; end Parent_14.Private_Child_A_14; 

Specification of private child B in SPARK 2014:

 1 2 3 4 5 private package Parent_14.Private_Child_B_14 with SPARK_Mode is function H (X : Integer) return Integer; end Parent_14.Private_Child_B_14; 

Specification of public child A in SPARK 2014:

 1 2 3 4 5 package Parent_14.Public_Child_A_14 with SPARK_Mode is function G (X : Integer) return Integer; end Parent_14.Public_Child_A_14; 

Specification of public child B in SPARK 2014:

 1 2 3 4 5 package Parent_14.Public_Child_B_14 with SPARK_Mode is function H (X : Integer) return Integer; end Parent_14.Public_Child_B_14; 

Body of parent in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 with Parent_14.Private_Child_A_14, -- OK Parent_14.Public_Child_A_14; -- OK package body Parent_14 with SPARK_Mode is function F (X : Integer) return Integer is (Private_Child_A_14.F (X)); function G (X : Integer) return Integer is (Public_Child_A_14.G (X)); end Parent_14; 

Body of public child A in SPARK 2014:

 1 2 3 4 5 6 7 package body Parent_14.Public_Child_A_14 with SPARK_Mode is function G (X : Integer) return Integer is (if X <= 0 then 0 else Parent_14.F (X)); -- OK end Parent_14.Public_Child_A_14; 

Body of public child B in SPARK 2014:

 1 2 3 4 5 6 7 8 with Parent_14.Private_Child_B_14; package body Parent_14.Public_Child_B_14 with SPARK_Mode is function H (X : Integer) return Integer is (Parent_14.Private_Child_B_14.H (X)); end Parent_14.Public_Child_B_14; 

Body of private child B in SPARK 2014:

 1 2 3 4 5 6 7 package body Parent_14.Private_Child_B_14 with SPARK_Mode is function H (X : Integer) return Integer is (if X <= 10 then 10 else Parent_14.F (X)); -- Legal in SPARK 2014 end Parent_14.Private_Child_B_14; 

### Abstract State Machines (ASMs)¶

#### Visible, concrete state¶

##### 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:

  1 2 3 4 5 6 7 8 9 10 package Stack_05 --# own S, Pointer; -- concrete state --# initializes S, Pointer; is procedure Push(X : in Integer); --# global in out S, Pointer; procedure Pop(X : out Integer); --# global in S; in out Pointer; end Stack_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 package body Stack_05 is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector := Vector'(Index_Range => 0); -- Initialization of S Pointer : Pointer_Range := 0; -- Initialization of Pointer procedure Push(X : in Integer) is begin Pointer := Pointer + 1; S(Pointer) := X; end Push; procedure Pop(X : out Integer) is begin X := S(Pointer); Pointer := Pointer - 1; end Pop; end Stack_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 package Stack_14 with SPARK_Mode, Abstract_State => (S_State, Pointer_State), Initializes => (S_State, Pointer_State) is procedure Push(X : in Integer) with Global => (In_Out => (S_State, Pointer_State)); procedure Pop(X : out Integer) with Global => (Input => S_State, In_Out => Pointer_State); end Stack_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 package body Stack_14 with SPARK_Mode, Refined_State => (S_State => S, Pointer_State => Pointer) is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector := Vector'(Index_Range => 0); -- Initialization of S Pointer : Pointer_Range := 0; -- Initialization of Pointer procedure Push (X : in Integer) with Refined_Global => (In_Out => (S, Pointer)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop(X : out Integer) with Refined_Global => (Input => S, In_Out => Pointer) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; end Stack_14; 
##### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 package body Stack_05 is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector; Pointer : Pointer_Range; procedure Push(X : in Integer) is begin Pointer := Pointer + 1; S(Pointer) := X; end Push; procedure Pop(X : out Integer) is begin X := S(Pointer); Pointer := Pointer - 1; end Pop; begin -- initialization Pointer := 0; S := Vector'(Index_Range => 0); end Stack_05; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 package body Stack_14 with SPARK_Mode, Refined_State => (S_State => S, Pointer_State => Pointer) is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector; Pointer : Pointer_Range; procedure Push (X : in Integer) with Refined_Global => (In_Out => (S, Pointer)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop(X : out Integer) with Refined_Global => (Input => S, In_Out => Pointer) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; begin -- initialization Pointer := 0; S := Vector'(Index_Range => 0); end Stack_14; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 package Stack_05 --# own S, Pointer; is procedure Push(X : in Integer); --# global in out S, Pointer; procedure Pop(X : out Integer); --# global in S; --# in out Pointer; private Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector; Pointer : Pointer_Range; end Stack_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 package Stack_14 with SPARK_Mode, Abstract_State => (S_State, Pointer_State) is procedure Push(X : in Integer) with Global => (In_Out => (S_State, Pointer_State)); procedure Pop(X : out Integer) with Global => (Input => S_State, In_Out => Pointer_State); private Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector with Part_Of => S_State; Pointer : Pointer_Range with Part_Of => Pointer_State; end Stack_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 package body Stack_14 with SPARK_Mode, Refined_State => (S_State => S, Pointer_State => Pointer) is procedure Push(X : in Integer) with Refined_Global => (In_Out => (S, Pointer)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop (X : out Integer) with Refined_Global => (Input => S, In_Out => Pointer) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; end Stack_14; 

#### Private, abstract state, refining onto concrete states in body¶

##### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package Stack_05 --# own State; is procedure Push(X : in Integer); --# global in out State; procedure Pop(X : out Integer); --# global in out State; procedure Init; --# global out State; end Stack_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 package body Stack_05 --# own State is S, Pointer; is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; Pointer : Pointer_Range; S : Vector; procedure Push(X : in Integer) --# global in out Pointer, S; is begin Pointer := Pointer + 1; S(Pointer) := X; end Push; procedure Pop(X : out Integer) --# global in S; --# in out Pointer; is begin X := S(Pointer); Pointer := Pointer - 1; end Pop; procedure Init --# global out Pointer, S; is begin Pointer := 0; S := Vector'(Index_Range => 0); end Init; end Stack_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package Stack_14 with SPARK_Mode, Abstract_State => State is procedure Push(X : in Integer) with Global => (In_Out => State); procedure Pop(X : out Integer) with Global => (In_Out => State); procedure Init with Global => (Output => State); end Stack_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 package body Stack_14 with SPARK_Mode, Refined_State => (State => (Pointer, S)) is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; Pointer : Pointer_Range; S : Vector; procedure Push(X : in Integer) with Refined_Global => (In_Out => (Pointer, S)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop (X : out Integer) with Refined_Global => (In_Out => Pointer, Input => S) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; procedure Init with Refined_Global => (Output => (Pointer, S)) is begin Pointer := 0; S := (Index_Range => 0); end Init; end Stack_14; 
##### 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:

  1 2 3 4 5 6 7 8 9 10 11 package Stack_05 --# own State; --# initializes State; is procedure Push(X : in Integer); --# global in out State; procedure Pop(X : out Integer); --# global in out State; end Stack_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 package body Stack_05 --# own State is Pointer, S; -- refinement of state is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector := Vector'(others => 0); Pointer : Pointer_Range := 0; -- initialization by elaboration of declaration procedure Push(X : in Integer) --# global in out Pointer, S; is begin Pointer := Pointer + 1; S(Pointer) := X; end Push; procedure Pop(X : out Integer) --# global in S; --# in out Pointer; is begin X := S(Pointer); Pointer := Pointer - 1; end Pop; end Stack_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 package Stack_14 with SPARK_Mode, Abstract_State => State, Initializes => State is procedure Push(X : in Integer) with Global => (In_Out => State); procedure Pop(X : out Integer) with Global => (In_Out => State); end Stack_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 package body Stack_14 with SPARK_Mode, Refined_State => (State => (Pointer, S)) -- refinement of state is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector := (others => 0); Pointer : Pointer_Range := 0; -- initialization by elaboration of declaration procedure Push(X : in Integer) with Refined_Global => (In_Out => (Pointer, S)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop(X : out Integer) with Refined_Global => (In_Out => Pointer, Input => S) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; end Stack_14; 
##### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 package body Stack_05 --# own State is Pointer, S; -- refinement of state is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector; Pointer : Pointer_Range; procedure Push(X : in Integer) --# global in out Pointer, S; is begin Pointer := Pointer + 1; S(Pointer) := X; end Push; procedure Pop(X : out Integer) --# global in out Pointer; --# in S; is begin X := S(Pointer); Pointer := Pointer - 1; end Pop; begin -- initialized by package body statements Pointer := 0; S := Vector'(Index_Range => 0); end Stack_05; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 package body Stack_14 with SPARK_Mode, Refined_State => (State => (Pointer, S)) -- refinement of state is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector; Pointer : Pointer_Range; procedure Push(X : in Integer) with Refined_Global => (In_Out => (Pointer, S)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop(X : out Integer) with Refined_Global => (In_Out => Pointer, Input => S) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; begin -- initialized by package body statements Pointer := 0; S := (Index_Range => 0); end Stack_14; 
##### 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:

  1 2 3 4 5 6 7 8 9 10 11 package Stack_05 --# own Stack; --# initializes Stack; is procedure Push(X : in Integer); --# global in out Stack; procedure Pop(X : out Integer); --# global in out Stack; end Stack_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 package body Stack_05 --# own Stack is S, Pointer; -- state refinement is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector; Pointer : Pointer_Range := 0; -- initialization by elaboration of declaration procedure Push(X : in Integer) --# global in out S, Pointer; is begin Pointer := Pointer + 1; S(Pointer) := X; end Push; procedure Pop(X : out Integer) --# global in S; --# in out Pointer; is begin X := S(Pointer); Pointer := Pointer - 1; end Pop; begin -- initialization by body statements S := Vector'(Index_Range => 0); end Stack_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 package Stack_14 with SPARK_Mode, Abstract_State => Stack, Initializes => Stack is procedure Push(X : in Integer) with Global => (In_Out => Stack); procedure Pop(X : out Integer) with Global => (In_Out => Stack); end Stack_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 package body Stack_14 with SPARK_Mode, Refined_State => (Stack => (S, Pointer)) -- state refinement is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; S : Vector; -- left uninitialized Pointer : Pointer_Range := 0; -- initialization by elaboration of declaration procedure Push(X : in Integer) with Refined_Global => (In_Out => (S, Pointer)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop (X : out Integer) with Refined_Global => (Input => S, In_Out => Pointer) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; begin -- partial initialization by body statements S := (Index_Range => 0); end Stack_14; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 package Stack_14 with SPARK_Mode, Abstract_State => State, Initializes => State, Initial_Condition => Is_Empty -- Stating that Is_Empty holds -- after initialization is function Is_Empty return Boolean with Global => State; function Is_Full return Boolean with Global => State; function Top return Integer with Global => State, Pre => not Is_Empty; procedure Push (X: in Integer) with Global => (In_Out => State), Pre => not Is_Full, Post => Top = X; procedure Pop (X: out Integer) with Global => (In_Out => State), Pre => not Is_Empty; end Stack_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 package body Stack_14 with SPARK_Mode, Refined_State => (State => (S, Pointer)) -- State refinement is Max_Stack_Size : constant := 1024; type Pointer_Range is range 0 .. Max_Stack_Size; subtype Index_Range is Pointer_Range range 1 .. Max_Stack_Size; type Vector is array (Index_Range) of Integer; -- Declaration of constituents S : Vector; Pointer : Pointer_Range; -- The subprogram contracts are refined in terms of the constituents. -- Expression functions could be used where applicable function Is_Empty return Boolean is (Pointer = 0) with Refined_Global => Pointer; function Is_Full return Boolean is (Pointer = Max_Stack_Size) with Refined_Global => Pointer; function Top return Integer is (S (Pointer)) with Refined_Global => (Pointer, S); procedure Push(X: in Integer) with Refined_Global => (In_Out => (Pointer, S)) is begin Pointer := Pointer + 1; S (Pointer) := X; end Push; procedure Pop(X: out Integer) with Refined_Global => (Input => S, In_Out => Pointer) is begin X := S (Pointer); Pointer := Pointer - 1; end Pop; begin -- Initialization - we promised to initialize the state -- and that initially the stack will be empty Pointer := 0; -- Is_Empty is True. S := Vector'(Index_Range => 0); end Stack_14; 

#### 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:

 1 2 3 4 5 6 7 8 9 -- Use of child packages to encapsulate state package Power_05 --# own State; --# initializes State; is procedure Read_Power(Level : out Integer); --# global State; --# derives Level from State; end Power_05; 

Body of Parent in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 with Power_05.Source_A_05, Power_05.Source_B_05; package body Power_05 --# own State is Power_05.Source_A_05.State, --# Power_05.Source_B_05.State; is procedure Read_Power(Level : out Integer) --# global Source_A_05.State, Source_B_05.State; --# derives --# Level --# from --# Source_A_05.State, --# Source_B_05.State; is Level_A : Integer; Level_B : Integer; begin Source_A_05.Read (Level_A); Source_B_05.Read (Level_B); Level := Level_A + Level_B; end Read_Power; end Power_05; 

Specifications of Private Children in SPARK 2005:

 1 2 3 4 5 6 7 8 9 --# inherit Power_05; private package Power_05.Source_A_05 --# own State; --# initializes State; is procedure Read (Level : out Integer); --# global State; --# derives Level from State; end Power_05.Source_A_05; 
 1 2 3 4 5 6 7 8 9 --# inherit Power_05; private package Power_05.Source_B_05 --# own State; --# initializes State; is procedure Read (Level : out Integer); --# global State; --# derives Level from State; end Power_05.Source_B_05; 

Bodies of Private Children in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package body Power_05.Source_A_05 --# own State is S; is S : Integer := 0; procedure Read (Level : out Integer) --# global in S; --# derives Level from S; is begin Level := S; end Read; end Power_05.Source_A_05; 
  1 2 3 4 5 6 7 8 9 10 11 12 13 package body Power_05.Source_B_05 --# own State is S; is S : Integer := 0; procedure Read (Level : out Integer) --# global in S; --# derives Level from S; is begin Level := S; end Read; end Power_05.Source_B_05; 

Specification of Parent in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 -- Use of child packages to encapsulate state package Power_14 with SPARK_Mode, Abstract_State => State, Initializes => State is procedure Read_Power(Level : out Integer) with Global => State, Depends => (Level => State); end Power_14; 

Body of Parent in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 with Power_14.Source_A_14, Power_14.Source_B_14; package body Power_14 with SPARK_Mode, Refined_State => (State => (Power_14.Source_A_14.State, Power_14.Source_B_14.State)) is procedure Read_Power(Level : out Integer) with Refined_Global => (Source_A_14.State, Source_B_14.State), Refined_Depends => (Level => (Source_A_14.State, Source_B_14.State)) is Level_A : Integer; Level_B : Integer; begin Source_A_14.Read (Level_A); Source_B_14.Read (Level_B); Level := Level_A + Level_B; end Read_Power; end Power_14; 

Specifications of Private Children in SPARK 2014:

 1 2 3 4 5 6 7 8 9 private package Power_14.Source_A_14 with SPARK_Mode, Abstract_State => (State with Part_Of =>Power_14.State), Initializes => State is procedure Read (Level : out Integer) with Global => State, Depends => (Level => State); end Power_14.Source_A_14; 
 1 2 3 4 5 6 7 8 9 private package Power_14.Source_B_14 with SPARK_Mode, Abstract_State => (State with Part_Of => Power_14.State), Initializes => State is procedure Read (Level : out Integer) with Global => State, Depends => (Level => State); end Power_14.Source_B_14; 

Bodies of Private Children in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 package body Power_14.Source_A_14 with SPARK_Mode, Refined_State => (State => S) is S : Integer := 0; procedure Read (Level : out Integer) with Refined_Global => (Input => S), Refined_Depends => (Level => S) is begin Level := S; end Read; end Power_14.Source_A_14; 
  1 2 3 4 5 6 7 8 9 10 11 12 13 14 package body Power_14.Source_B_14 with SPARK_Mode, Refined_State => (State => S) is S : Integer := 0; procedure Read (Level : out Integer) with Refined_Global => (Input => S), Refined_Depends => (Level => S) is begin Level := S; end Read; end Power_14.Source_B_14; 

#### Private, abstract state, refining onto concrete state of embedded package¶

This example is based around the packages from section Private, abstract state, refining onto concrete state of embedded package, with the private child packages converted into embedded packages and the refinement onto concrete visible state.

Specification in SPARK 2005:

 1 2 3 4 5 6 7 8 -- Use of embedded packages to encapsulate state package Power_05 --# own State; is procedure Read_Power(Level : out Integer); --# global State; --# derives Level from State; end Power_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 package body Power_05 --# own State is Source_A.State, --# Source_B.State; is -- Embedded package spec for Source_A package Source_A --# own State; is procedure Read (Level : out Integer); --# global State; --# derives Level from State; end Source_A; -- Embedded package spec for Source_B. package Source_B --# own State; is procedure Read (Level : out Integer); --# global State; --# derives Level from State; end Source_B; -- Embedded package body for Source_A package body Source_A is State : Integer; procedure Read (Level : out Integer) is begin Level := State; end Read; end Source_A; -- Embedded package body for Source_B package body Source_B is State : Integer; procedure Read (Level : out Integer) is begin Level := State; end Read; end Source_B; procedure Read_Power(Level : out Integer) --# global Source_A.State, Source_B.State; --# derives --# Level --# from --# Source_A.State, --# Source_B.State; is Level_A : Integer; Level_B : Integer; begin Source_A. Read (Level_A); Source_B.Read (Level_B); Level := Level_A + Level_B; end Read_Power; end Power_05; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 -- Use of embedded packages to encapsulate state package Power_14 with SPARK_Mode, Abstract_State => State, Initializes => State is procedure Read_Power(Level : out Integer) with Global => State, Depends => (Level => State); end Power_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 package body Power_14 with SPARK_Mode, Refined_State => (State => (Source_A.State, Source_B.State)) is -- Embedded package spec for Source_A package Source_A with Initializes => State is State : Integer := 0; procedure Read (Level : out Integer) with Global => State, Depends => (Level => State); end Source_A; -- Embedded package spec for Source_B. package Source_B with Initializes => State is State : Integer := 0; procedure Read (Level : out Integer) with Global => State, Depends => (Level => State); end Source_B; -- Embedded package body for Source_A package body Source_A is procedure Read (Level : out Integer) is begin Level := State; end Read; end Source_A; -- Embedded package body for Source_B package body Source_B is procedure Read (Level : out Integer) is begin Level := State; end Read; end Source_B; procedure Read_Power(Level : out Integer) with Refined_Global => (Source_A.State, Source_B.State), Refined_Depends => (Level => (Source_A.State, Source_B.State)) is Level_A : Integer; Level_B : Integer; begin Source_A. Read (Level_A); Source_B.Read (Level_B); Level := Level_A + Level_B; end Read_Power; end Power_14; 

#### Private, abstract state, refining onto mixture of the above¶

This example is based around the packages from sections Private, abstract state, refining onto state of private child and Private, abstract state, refining onto concrete state of embedded package. 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¶

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 with Input_Port_05, Output_Port_05, Stacks_05; --# inherit Input_Port_05, Output_Port_05, Stacks_05; --# main_program; procedure Copy_05 --# global in Input_Port_05.Input_State; --# out Output_Port_05.Output_State; --# derives Output_Port_05.Output_State from Input_Port_05.Input_State; is The_Stack : Stacks_05.Stack; Value : Integer; Done : Boolean; Final_Value : constant Integer := 999; begin Stacks_05.Clear(The_Stack); loop Input_Port_05.Read_From_Port(Value); Stacks_05.Push(The_Stack, Value); Done := Value = Final_Value; exit when Done; end loop; loop Stacks_05.Pop(The_Stack, Value); Output_Port_05.Write_To_Port(Value); exit when Stacks_05.Is_Empty(The_Stack); end loop; end Copy_05; 

Specification of input port in SPARK 2005:

 1 2 3 4 5 6 7 8 package Input_Port_05 --# own in Input_State; is procedure Read_From_Port(Input_Value : out Integer); --# global in Input_State; --# derives Input_Value from Input_State; end Input_Port_05; 

Body of input port in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 package body Input_Port_05 is Input_State : Integer; for Input_State'Address use System.Storage_Elements.To_Address (16#ACECAE0#); pragma Volatile (Input_State); procedure Read_From_Port(Input_Value : out Integer) is begin Input_Value := Input_State; end Read_From_Port; end Input_Port_05; 

Specification of output port in SPARK 2005:

 1 2 3 4 5 6 7 package Output_Port_05 --# own out Output_State; is procedure Write_To_Port(Output_Value : in Integer); --# global out Output_State; --# derives Output_State from Output_Value; end Output_Port_05; 

Body of output port in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 package body Output_Port_05 is Output_State : Integer; for Output_State'Address use System.Storage_Elements.To_Address (16#ACECAF0#); pragma Volatile (Output_State); procedure Write_To_Port(Output_Value : in Integer) is begin Output_State := Output_Value; end Write_To_Port; end Output_Port_05; 

Specification of main program in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 with Input_Port_14, Output_Port_14, Stacks_14; -- No need to specify that Copy_14 is a main program procedure Copy_14 with SPARK_Mode, Global => (Input => Input_Port_14.Input_State, Output => Output_Port_14.Output_State), Depends => (Output_Port_14.Output_State => Input_Port_14.Input_State) is The_Stack : Stacks_14.Stack; Value : Integer; Done : Boolean; Final_Value : constant Integer := 999; begin Stacks_14.Clear(The_Stack); loop Input_Port_14.Read_From_Port(Value); Stacks_14.Push(The_Stack, Value); Done := Value = Final_Value; exit when Done; end loop; loop Stacks_14.Pop(The_Stack, Value); Output_Port_14.Write_To_Port(Value); exit when Stacks_14.Is_Empty(The_Stack); end loop; end Copy_14; 

Specification of input port in SPARK 2014:

 1 2 3 4 5 6 7 8 package Input_Port_14 with SPARK_Mode, Abstract_State => (Input_State with External => Async_Writers) is procedure Read_From_Port(Input_Value : out Integer) with Global => (Input => Input_State), Depends => (Input_Value => Input_State); end Input_Port_14; 

Specification of output port in SPARK 2014:

 1 2 3 4 5 6 7 8 package Output_Port_14 with SPARK_Mode, Abstract_State => (Output_State with External => Async_Readers) is procedure Write_To_Port(Output_Value : in Integer) with Global => (Output => Output_State), Depends => (Output_State => Output_Value); end Output_Port_14; 

Body of input port in SPARK 2014:

This is as per SPARK 2005, but uses aspects instead of representation clauses and pragmas.

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 with System.Storage_Elements; package body Input_Port_14 with SPARK_Mode, Refined_State => (Input_State => Input_S) is Input_S : Integer with Volatile, Async_Writers, Address => System.Storage_Elements.To_Address (16#ACECAE0#); procedure Read_From_Port(Input_Value : out Integer) with Refined_Global => (Input => Input_S), Refined_Depends => (Input_Value => Input_S) is begin Input_Value := Input_S; end Read_From_Port; end Input_Port_14; 

Body of output port in SPARK 2014:

This is as per SPARK 2005, but uses aspects instead of representation clauses and pragmas.

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 with System.Storage_Elements; package body Output_Port_14 with SPARK_Mode, Refined_State => (Output_State => Output_S) is Output_S : Integer with Volatile, Async_Readers, Address => System.Storage_Elements.To_Address (16#ACECAF0#); procedure Write_To_Port(Output_Value : in Integer) with Refined_Global => (Output => Output_S), Refined_Depends => (Output_S => Output_Value) is begin Output_S := Output_Value; end Write_To_Port; end Output_Port_14; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 package Input_Port --# own in Inputs : Integer; is procedure Read_From_Port(Input_Value : out Integer); --# global in Inputs; --# derives Input_Value from Inputs; --# post (Inputs~ = 0 -> (Input_Value = Inputs'Tail (Inputs~))) and --# (Inputs~ /= 0 -> (Input_Value = Inputs~)); end Input_Port; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 package body Input_Port is Inputs : Integer; for Inputs'Address use System.Storage_Elements.To_Address (16#ACECAF0#); --# assert Inputs'Always_Valid; pragma Volatile (Inputs); procedure Read_From_Port(Input_Value : out Integer) is begin Input_Value := Inputs; if Input_Value = 0 then Input_Value := Inputs; end if; end Read_From_Port; end Input_Port; 

Specification in SPARK 2014:

 1 2 3 4 5 6 7 8 package Input_Port_14 with SPARK_Mode, Abstract_State => (Inputs with External => Async_Writers) is procedure Read_From_Port(Input_Value : out Integer) with Global => Inputs, Depends => (Input_Value => Inputs); end Input_Port_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 with System.Storage_Elements; package body Input_Port_14 with SPARK_Mode, Refined_State => (Inputs => Input_Port) is Input_Port : Integer with Volatile, Async_Writers, Address => System.Storage_Elements.To_Address (16#ACECAF0#); procedure Read_From_Port(Input_Value : out Integer) with Refined_Global => Input_Port, Refined_Depends => (Input_Value => Input_Port) is First_Read : Integer; Second_Read : Integer; begin Second_Read := Input_Port; -- Ensure Second_Read is initialized pragma Assume (Second_Read'Valid); First_Read := Second_Read; -- but it is infact the First_Read. if First_Read = 0 then Second_Read := Input_Port; -- Now it is the Second_Read pragma Assume (Second_Read'Valid); Input_Value := Second_Read; else Input_Value := First_Read; end if; pragma Assert ((First_Read = 0 and then Input_Value = Second_Read) or else (Input_Value = First_Read)); end Read_From_Port; end Input_Port_14; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 package Output_Port --# own out Outputs : Integer; is procedure Write_To_Port(Output_Value : in Integer); --# global out Outputs; --# derives Outputs from Output_Value; --# post ((Output_Value = -1) -> --# (Outputs = --# Outputs'Append (Outputs'Append (Outputs~, 0), Output_Value))) --# and --# ((Output_Value /= -1) -> --# (Outputs = --# Outputs'Append (Outputs~, Output_Value))); end Output_Port; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 package body Output_Port is Outputs : Integer; for Outputs'Address use System.Storage_Elements.To_Address (16#ACECAF10#); pragma Volatile (Outputs); procedure Write_To_Port(Output_Value : in Integer) is begin if Output_Value = -1 then Outputs := 0; end if; Outputs := Output_Value; end Write_To_Port; end Output_Port; 

Specification in SPARK 2014:

 1 2 3 4 5 6 7 8 package Output_Port_14 with SPARK_Mode, Abstract_State => (Outputs with External => Async_Readers) is procedure Write_To_Port(Output_Value : in Integer) with Global => (Output => Outputs), Depends => (Outputs => Output_Value); end Output_Port_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 with System.Storage_Elements; package body Output_Port_14 with SPARK_Mode, Refined_State => (Outputs => Output_Port) is Output_Port : Integer with Volatile, Async_Readers, Address => System.Storage_Elements.To_Address (16#ACECAF10#); -- This is a simple subprogram that always updates the Output_Shadow with -- the single value which is written to the output port. procedure Write_It (Output_Value : in Integer; Output_Shadow : out Integer) with Global => (Output => Output_Port), Depends => ((Output_Port, Output_Shadow) => Output_Value), Post => Output_Shadow = Output_Value is begin Output_Shadow := Output_Value; Output_Port := Output_Shadow; end Write_It; procedure Write_To_Port(Output_Value : in Integer) with Refined_Global => (Output => Output_Port), Refined_Depends => (Output_Port => Output_Value) is Out_1, Out_2 : Integer; begin if Output_Value = -1 then Write_It (0, Out_1); Write_It (Output_Value, Out_2); else Write_It (Output_Value, Out_1); Out_2 := Out_1; -- Avoids flow error. end if; pragma Assert (if Output_Value = -1 then Out_1 = 0 and Out_2 = Output_Value else Out_1 = Output_Value); end Write_To_Port; end Output_Port_14; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 package Switch --# own in State; is type Reading is (on, off, unknown); function ReadValue return Reading; --# global in State; end Switch; 

Component Switch specifications in SPARK 2005:

 1 2 3 4 5 6 7 8 --# inherit Switch; private package Switch.Val1 --# own in State; is function Read return Switch.Reading; --# global in State; end Switch.Val1; 
 1 2 3 4 5 6 7 8 --# inherit Switch; private package Switch.Val2 --# own in State; is function Read return Switch.Reading; --# global in State; end Switch.Val2; 
 1 2 3 4 5 6 7 8 --# inherit Switch; private package Switch.Val3 --# own in State; is function Read return Switch.Reading; --# global in State; end Switch.Val3; 

Switch body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 with Switch.Val1; with Switch.Val2; with Switch.Val3; package body Switch --# own State is in Switch.Val1.State, --# in Switch.Val2.State, --# in Switch.Val3.State; is subtype Value is Integer range -1 .. 1; subtype Score is Integer range -3 .. 3; type ConvertToValueArray is array (Reading) of Value; type ConvertToReadingArray is array (Score) of Reading; ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(on => 1, unknown => 0, off => -1); ConvertToReading : constant ConvertToReadingArray := ConvertToReadingArray'(-3 .. -2 => off, -1 .. 1 => unknown, 2 ..3 => on); function ReadValue return Reading --# global in Val1.State; --# in Val2.State; --# in Val3.State; is A, B, C : Reading; begin A := Val1.Read; B := Val2.Read; C := Val3.Read; return ConvertToReading (ConvertToValue (A) + ConvertToValue (B) + ConvertToValue (C)); end ReadValue; end Switch; 

Abstract Switch specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 package Switch with SPARK_Mode, Abstract_State => (State with External => Async_Writers) is type Reading is (on, off, unknown); function ReadValue return Reading with Volatile_Function, Global => (Input => State); end Switch; 

Component Switch specifications in SPARK 2014:

 1 2 3 4 5 6 7 8 9 private package Switch.Val1 with SPARK_Mode, Abstract_State => (State with External => Async_Writers, Part_Of => Switch.State) is function Read return Switch.Reading with Volatile_Function, Global => (Input => State); end Switch.Val1; 
 1 2 3 4 5 6 7 8 9 private package Switch.Val2 with SPARK_Mode, Abstract_State => (State with External => Async_Writers, Part_Of => Switch.State) is function Read return Switch.Reading with Volatile_Function, Global => (Input => State); end Switch.Val2; 
 1 2 3 4 5 6 7 8 9 private package Switch.Val3 with SPARK_Mode, Abstract_State => (State with External => Async_Writers, Part_Of => Switch.State) is function Read return Switch.Reading with Volatile_Function, Global => (Input => State); end Switch.Val3; 

Switch body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 with Switch.Val1, Switch.Val2, Switch.Val3; package body Switch -- State is refined onto three states, each of which has properties -- Volatile and Input with SPARK_Mode, Refined_State => (State => (Switch.Val1.State, Switch.Val2.State, Switch.Val3.State)) is subtype Value is Integer range -1 .. 1; subtype Score is Integer range -3 .. 3; type ConvertToValueArray is array (Reading) of Value; type ConvertToReadingArray is array (Score) of Reading; ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(on => 1, unknown => 0, off => -1); ConvertToReading : constant ConvertToReadingArray := ConvertToReadingArray'(-3 .. -2 => off, -1 .. 1 => unknown, 2 .. 3 => on); function ReadValue return Reading with Refined_Global => (Input => (Val1.State, Val2.State, Val3.State)) is A, B, C : Reading; begin A := Val1.Read; B := Val2.Read; C := Val3.Read; return ConvertToReading (ConvertToValue (A) + ConvertToValue (B) + ConvertToValue (C)); end ReadValue; end Switch; 

#### 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:

 1 2 3 4 5 6 7 8 package Device --# own State; --# initializes State; is procedure Write (X : in Integer); --# global in out State; --# derives State from State, X; end Device; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 package body Device --# own State is OldX, --# in StatusPort, --# out Register; -- refinement on to mix of external and ordinary variables is type Status_Port_Type is mod 2**32; OldX : Integer := 0; -- only component that needs initialization StatusPort : Status_Port_Type; pragma Volatile (StatusPort); -- address clause would be added here Register : Integer; pragma Volatile (Register); -- address clause would be added here procedure WriteReg (X : in Integer) --# global out Register; --# derives Register from X; is begin Register := X; end WriteReg; procedure ReadAck (OK : out Boolean) --# global in StatusPort; --# derives OK from StatusPort; is RawValue : Status_Port_Type; begin RawValue := StatusPort; -- only assignment allowed here OK := RawValue = 16#FFFF_FFFF#; end ReadAck; procedure Write (X : in Integer) --# global in out OldX; --# out Register; --# in StatusPort; --# derives OldX,Register from OldX, X & --# null from StatusPort; is OK : Boolean; begin if X /= OldX then OldX := X; WriteReg (X); loop ReadAck (OK); exit when OK; end loop; end if; end Write; end Device; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 package Device with SPARK_Mode, Abstract_State => (State with External => (Async_Readers, Async_Writers)), Initializes => State is procedure Write (X : in Integer) with Global => (In_Out => State), Depends => (State =>+ X); end Device; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 package body Device with SPARK_Mode, Refined_State => (State => (OldX, StatusPort, Register)) -- refinement on to mix of external and ordinary variables is type Status_Port_Type is mod 2**32; OldX : Integer := 0; -- only component that needs initialization StatusPort : Status_Port_Type with Volatile, Async_Writers; -- address clause would be added here Register : Integer with Volatile, Async_Readers; -- address clause would be added here procedure WriteReg (X : in Integer) with Global => (Output => Register), Depends => (Register => X) is begin Register := X; end WriteReg; procedure ReadAck (OK : out Boolean) with Global => (Input => StatusPort), Depends => (OK => StatusPort) is RawValue : Status_Port_Type; begin RawValue := StatusPort; -- only assignment allowed here OK := RawValue = 16#FFFF_FFFF#; end ReadAck; procedure Write (X : in Integer) with Refined_Global => (Input => StatusPort, Output => Register, In_Out => OldX), Refined_Depends => ((OldX, Register) => (OldX, X), null => StatusPort) is OK : Boolean; begin if X /= OldX then OldX := X; WriteReg (X); loop ReadAck (OK); exit when OK; end loop; end if; end Write; end Device; 

#### 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 Input driver using 'Tail in a contract. 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:

 1 2 3 4 5 6 7 8 9  package Inc --# own in Sensor : Integer; is procedure Increases (Result : out Boolean; Valid : out Boolean); --# global in Sensor; --# post Valid -> (Result <-> Sensor'Tail (Sensor~) > Sensor~); end Inc; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 with System.Storage_Elements; package body Inc -- Cannot refine own variable Sensor as it has been given a concrete type. is Sensor : Integer; for Sensor'Address use System.Storage_Elements.To_Address (16#DEADBEE0#); pragma Volatile (Sensor); procedure Read (V : out Integer; Valid : out Boolean) --# global in Sensor; --# post (Valid -> V = Sensor~) and --# (Sensor = Sensor'Tail (Sensor~)); is Tmp : Integer; begin Tmp := Sensor; if Tmp'Valid then V := Tmp; Valid := True; --# check Sensor = Sensor'Tail (Sensor~); else V := 0; Valid := False; end if; end Read; procedure Increases (Result : out Boolean; Valid : out Boolean) is A, B : Integer; begin Result := False; Read (A, Valid); if Valid then Read (B, Valid); if Valid then Result := B > A; end if; end if; end Increases; end Inc; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 package Inc with SPARK_Mode, Abstract_State => (Sensor with External => Async_Writers) is -- Declare a private type which will keep a trace of the -- values read. type Increasing_Indicator is private; -- Access (ghost) functions for the private type only intended for -- use in pre and post conditions or other assertion expressions function First (Indicator : Increasing_Indicator) return Integer with Ghost; function Second (Indicator : Increasing_Indicator) return Integer with Ghost; -- Used to check that the value returned by procedure Increases -- is valid (Invalid values have not been read from the Sensor). function Is_Valid (Indicator : Increasing_Indicator) return Boolean; -- Use this function to determine whether the result of the procedure -- Increases indicates an increasing value. -- It can only be called if Is_Valid (Indicator) function Is_Increasing (Indicator : Increasing_Indicator) return Boolean with Pre => Is_Valid (Indicator); procedure Increases (Result : out Increasing_Indicator) with Global => Sensor, Post => (if Is_Valid (Result) then Is_Increasing (Result)= (Second (Result) > First (Result))); private type Increasing_Indicator is record Valid : Boolean; First, Second : Integer; end record; end Inc; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 with System.Storage_Elements; package body Inc with SPARK_Mode, Refined_State => (Sensor => S) is pragma Warnings (Off); S : Integer with Volatile, Async_Writers, Address => System.Storage_Elements.To_Address (16#DEADBEE0#); pragma Warnings (On); function First (Indicator : Increasing_Indicator) return Integer is (Indicator.First); function Second (Indicator : Increasing_Indicator) return Integer is (Indicator.Second); function Is_Valid (Indicator : Increasing_Indicator) return Boolean is (Indicator.Valid); function Is_Increasing (Indicator : Increasing_Indicator) return Boolean is (Indicator.Second > Indicator.First); pragma Warnings (Off); procedure Read (V : out Integer; Valid : out Boolean) with Global => S, Post => (if Valid then V'Valid) is Tmp : Integer; begin pragma Warnings (On); Tmp := S; pragma Warnings (Off); if Tmp'Valid then pragma Warnings (On); V := Tmp; Valid := True; else V := 0; Valid := False; end if; end Read; procedure Increases (Result : out Increasing_Indicator) with Refined_Global => S is begin Read (Result.First, Result.Valid); if Result.Valid then Read (Result.Second, Result.Valid); else Result.Second := 0; end if; end Increases; end Inc; 

### Package Inheritance¶

SPARK 2014 does not have the SPARK 2005 concept of package inheritance. It has the same package visibility rules as Ada.

#### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 package Raw_Data --# own State; --# Initializes State; is function Data_Is_Valid return Boolean; --# global State; function Get_Value return Integer; --# global State; procedure Read_Next; --# global in out State; --# derives State from State; end Raw_Data; 
  1 2 3 4 5 6 7 8 9 10 11 12 13 14 with Raw_Data; --# inherit Raw_Data; package Processing --# own State; --# Initializes State; is procedure Get_Processed_Data (Value : out Integer); --# global in Raw_Data.State; --# in out State; --# derives Value, State from State, Raw_Data.State; --# pre Raw_Data.Data_Is_Valid (Raw_Data.State); end Processing; 
  1 2 3 4 5 6 7 8 9 10 11 12 with Processing; --# inherit Processing, Raw_Data; package Calculate is procedure Read_Calculated_Value (Value : out Integer); --# global in out Processing.State; --# in Raw_Data.State; --# derives Value, Processing.State from Processing.State, Raw_Data.State; --# pre Raw_Data.Data_Is_Valid (Raw_Data.State); end Calculate; 

Specifications in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 package Raw_Data with SPARK_Mode, Abstract_State => (State with External => Async_Writers), Initializes => State is function Data_Is_Valid return Boolean with Volatile_Function, Global => State; function Get_Value return Integer with Volatile_Function, Global => State; procedure Read_Next with Global => (In_Out => State), Depends => (State => State); end Raw_Data; 
  1 2 3 4 5 6 7 8 9 10 11 12 13 14 with Raw_Data; package Processing with SPARK_Mode, Abstract_State => State is procedure Get_Processed_Data (Value : out Integer) with Global => (Input => Raw_Data.State, In_Out => State), Depends => ((Value, State) => (State, Raw_Data.State)), Pre => Raw_Data.Data_Is_Valid; end Processing; 
  1 2 3 4 5 6 7 8 9 10 11 12 13 14 with Processing, Raw_Data; package Calculate with SPARK_Mode is procedure Read_Calculated_Value (Value : out Integer) with Global => (In_Out => Processing.State, Input => Raw_Data.State), Depends => ((Value, Processing.State) => (Processing.State, Raw_Data.State)), Pre => Raw_Data.Data_Is_Valid; end Calculate; 

#### 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:

  1 2 3 4 5 6 7 8 9 10 package Switch --# own in State; is type Reading is (on, off, unknown); function ReadValue return Reading; --# global in State; end Switch; 

Component Switch specifications in SPARK 2005:

Switch body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 with Switch.Val1; with Switch.Val2; with Switch.Val3; package body Switch --# own State is in Switch.Val1.State, --# in Switch.Val2.State, --# in Switch.Val3.State; is subtype Value is Integer range -1 .. 1; subtype Score is Integer range -3 .. 3; function ReadValue return Reading --# global in Val1.State; --# in Val2.State; --# in Val3.State; is A, B, C : Reading; -- Embedded package to provide the capability to synthesize three inputs -- into one. --# inherit Switch; package Conversion is function Convert_To_Reading (Val_A : Switch.Reading; Val_B : Switch.Reading; Val_C : Switch.Reading) return Switch.Reading; end Conversion; package body Conversion is type ConvertToValueArray is array (Switch.Reading) of Switch.Value; type ConvertToReadingArray is array (Switch.Score) of Switch.Reading; ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(Switch.on => 1, Switch.unknown => 0, Switch.off => -1); ConvertToReading : constant ConvertToReadingArray := ConvertToReadingArray'(-3 .. -2 => Switch.off, -1 .. 1 => Switch.unknown, 2 ..3 => Switch.on); function Convert_To_Reading (Val_A : Switch.Reading; Val_B : Switch.Reading; Val_C : Switch.Reading) return Switch.Reading is begin return ConvertToReading (ConvertToValue (Val_A) + ConvertToValue (Val_B) + ConvertToValue (Val_C)); end Convert_To_Reading; end Conversion; begin A := Val1.Read; B := Val2.Read; C := Val3.Read; return Conversion.Convert_To_Reading (Val_A => A, Val_B => B, Val_C => C); end ReadValue; end Switch; 

Abstract Switch specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 package Switch with SPARK_Mode, Abstract_State => (State with External => Async_Writers) is type Reading is (on, off, unknown); function ReadValue return Reading with Volatile_Function, Global => (Input => State); end Switch; 

Component Switch specification in SPARK 2014:

Switch body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 with Switch.Val1, Switch.Val2, Switch.Val3; package body Switch -- State is refined onto three states, each of which has properties -- Volatile and Input. with SPARK_Mode, Refined_State => (State => (Switch.Val1.State, Switch.Val2.State, Switch.Val3.State)) is subtype Value is Integer range -1 .. 1; subtype Score is Integer range -3 .. 3; function ReadValue return Reading with Refined_Global => (Input => (Val1.State, Val2.State, Val3.State)) is A, B, C : Reading; -- Embedded package to provide the capability to synthesize three inputs -- into one. package Conversion is function Convert_To_Reading (Val_A : Switch.Reading; Val_B : Switch.Reading; Val_C : Switch.Reading) return Switch.Reading; end Conversion; package body Conversion is type ConvertToValueArray is array (Switch.Reading) of Switch.Value; type ConvertToReadingArray is array (Switch.Score) of Switch.Reading; ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(Switch.on => 1, Switch.unknown => 0, Switch.off => -1); ConvertToReading : constant ConvertToReadingArray := ConvertToReadingArray'(-3 .. -2 => Switch.off, -1 .. 1 => Switch.unknown, 2 .. 3 => Switch.on); function Convert_To_Reading (Val_A : Switch.Reading; Val_B : Switch.Reading; Val_C : Switch.Reading) return Switch.Reading is (ConvertToReading (ConvertToValue (Val_A) + ConvertToValue (Val_B) + ConvertToValue (Val_C))); end Conversion; begin -- begin statement of ReadValue function A := Val1.Read; B := Val2.Read; C := Val3.Read; return Conversion.Convert_To_Reading (Val_A => A, Val_B => B, Val_C => C); end ReadValue; end Switch; 

#### 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 suprogram.

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:

  1 2 3 4 5 6 7 8 9 10 package P_14 with SPARK_Mode, Abstract_State => P_State, Initializes => (P_State, Global_Var), Elaborate_Body is Global_Var : Integer; procedure Init (S : out Integer); end P_14; 
 1 2 3 4 5 6 7 8 9 package Q_14 with SPARK_Mode, Abstract_State => Q_State, Initializes => Q_State is type T is new Integer; procedure Init (S : out T); end Q_14; 
  1 2 3 4 5 6 7 8 9 10 11 with P_14; pragma Elaborate_All (P_14); -- Required because P_14.Global_Var -- Is mentioned as input in the Initializes aspect package R_14 with SPARK_Mode, Abstract_State => State, Initializes => (State => P_14.Global_Var) is procedure Op ( X : in Positive) with Global => (In_Out => State); end R_14; 

Package Bodies in SPARK 2014

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 with Q_14; package body P_14 with SPARK_Mode, Refined_State => (P_State => P_S) is P_S : Q_14.T; -- The use of type Q.T does not require -- the body of Q to be elaborated. procedure Init (S : out Integer) is begin S := 5; end Init; begin -- Cannot call Q_14.Init here beacuse -- this would require an Elaborate_All for Q_14 -- and would be detected as a circularity Init (Global_Var); P_S := Q_14.T (Global_Var); end P_14; 
  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 with P_14; pragma Elaborate_All (P_14); -- Required because the elaboration of the -- body of Q_14 (indirectly) calls P_14.Init package body Q_14 with SPARK_Mode, Refined_State => (Q_State => Q_S) is Q_S : T; procedure Init (S : out T) is V : Integer; begin P_14.Init (V); if V > 0 and then V <= Integer'Last - 5 then S := T(V + 5); else S := 5; end if; end Init; begin Init (Q_S); end Q_14; 
  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 with Q_14; pragma Elaborate_All (Q_14); -- Required because Q_14.Init is called -- in the elaboration of the body of R_14 use type Q_14.T; package body R_14 with SPARK_Mode, Refined_State => (State => R_S) is R_S : Q_14.T; procedure Op ( X : in Positive) with Refined_Global => (In_Out => R_S) is begin if R_S <= Q_14.T'Last - Q_14.T (X) then R_S := R_S + Q_14.T (X); else R_S := 0; end if; end Op; begin Q_14.Init (R_S); if P_14.Global_Var > 0 and then R_S <= Q_14.T'Last - Q_14.T (P_14.Global_Var) then R_S := R_S + Q_14.T (P_14.Global_Var); else R_S := Q_14.T (P_14.Global_Var); end if; end R_14; 

## Bodies and Proof¶

### Assert, Assume, Check contracts¶

#### 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:

 1 2 3 4 5 6 7 8 package Assert_Loop_05 is subtype Index is Integer range 1 .. 10; type A_Type is Array (Index) of Integer; function Value_present (A: A_Type; X : Integer) return Boolean; --# return for some M in Index => (A (M) = X); end Assert_Loop_05; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 package body Assert_Loop_05 is function Value_Present (A: A_Type; X : Integer) return Boolean is I : Index := Index'First; begin while A (I) /= X and I < Index'Last loop --# assert I < Index'Last and --# (for all M in Index range Index'First .. I => (A (M) /= X)); I := I + 1; end loop; return A (I) = X; end Value_Present; end Assert_Loop_05; 

Specification in SPARK 2014:

 1 2 3 4 5 6 7 8 9 package Assert_Loop_14 with SPARK_Mode is subtype Index is Integer range 1 .. 10; type A_Type is Array (Index) of Integer; function Value_present (A : A_Type; X : Integer) return Boolean with Post => Value_present'Result = (for some M in Index => A (M) = X); end Assert_Loop_14; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 package body Assert_Loop_14 with SPARK_Mode is function Value_Present (A : A_Type; X : Integer) return Boolean is I : Index := Index'First; begin while A (I) /= X and I < Index'Last loop pragma Loop_Invariant (I < Index'Last and (for all M in Index'First .. I => A (M) /= X)); I := I + 1; end loop; return A (I) = X; end Value_Present; end Assert_Loop_14; 

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

#### 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:

 1 2 3 4 5 6 7 8 package Input_Port --# own in Inputs; is procedure Read_From_Port(Input_Value : out Integer); --# global in Inputs; --# derives Input_Value from Inputs; end Input_Port; 

Body for Assume annotation in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 with System.Storage_Elements; package body Input_Port is Inputs : Integer; for Inputs'Address use System.Storage_Elements.To_Address (16#CAFE0#); pragma Volatile (Inputs); procedure Read_From_Port(Input_Value : out Integer) is begin --# assume Inputs in Integer; Input_Value := Inputs; end Read_From_Port; end Input_Port; 

Specification for Assume annotation in SPARK 2014:

 1 2 3 4 5 6 7 8 package Input_Port with SPARK_Mode, Abstract_State => (State_Inputs with External => Async_Writers) is procedure Read_From_Port(Input_Value : out Integer) with Global => (Input => State_Inputs), Depends => (Input_Value => State_Inputs); end Input_Port; 

Body for Assume annotation in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 with System.Storage_Elements; package body Input_Port with SPARK_Mode, Refined_State => (State_Inputs => Inputs) is Inputs : Integer with Volatile, Async_Writers, Address => System.Storage_Elements.To_Address (16#CAFE0#); procedure Read_From_Port(Input_Value : out Integer) with Refined_Global => (Input => Inputs), Refined_Depends => (Input_Value => Inputs) is begin Input_Value := Inputs; pragma Assume(Input_Value in Integer); end Read_From_Port; end Input_Port; 

#### 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:

 1 2 3 4 5 6 7 package Check_05 is subtype Small is Integer range 1 .. 10; subtype Big is Integer range 1 .. 21; procedure Compare(A, B : in Small; C : in out Big); end Check_05; 

Body for Check annotation in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package body Check_05 is procedure Compare(A, B : in Small; C : in out Big) is begin if (A + B >= C) then C := A; C := C + B; C := C + 1; end if; --# check A + B < C; end Compare; end Check_05; 

Specification for Check annotation in SPARK 2014:

 1 2 3 4 5 6 7 8 package Check_14 with SPARK_Mode is subtype Small is Integer range 1 .. 10; subtype Big is Integer range 1 .. 21; procedure Compare (A, B : in Small; C : in out Big); end Check_14; 

Body for Check annotation in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package body Check_14 with SPARK_Mode is procedure Compare(A, B : in Small; C : in out Big) is begin if A + B >= C then C := A; C := C + B; C := C + 1; end if; pragma Assert (A + B < C); end Compare; end Check_14; 

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

### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 package Stack --# own State : Abstract_Stack; is -- It is not possible to specify that the stack will be -- initialized to empty except by having an initialization -- subprogram called during program execution (as opposed to -- package elaboration). -- Proof functions to indicate whether or not the Stack is empty -- and whether or not it is full. --# type Abstract_Stack is abstract; --# function Max_Stack_Size return Natural; -- Proof function to give the number of elements on the stack. --# function Count(Input : Abstract_Stack) return Natural; -- Proof function returns the Nth entry on the stack. -- Stack_Entry (Count (State)) is the top of stack --# function Stack_Entry (N : Natural; S : Abstract_Stack) return Integer; --# pre N in 1 .. Count (S); -- A refined version of this function cannot be written because -- the abstract view has a formal parameter of type Abstract_Stack -- whereas the refined view would not have this parameter but use -- a global. A user defined proof rule would be required to define -- this function. Alternatively, it could be written as an Ada -- function where the the global and formal parameter views would -- be available. However, the function would then be callable and -- generate implementation code. --# function Is_Empty(Input : Abstract_Stack) return Boolean; --# return Count (Input) = 0; --# function Is_Full(Input : Abstract_Stack) return Boolean; --# return Count (Input) = Max_Stack_Size; -- The precondition requires the stack is not full when a value, X, -- is pushed onto it. -- The postcondition indicates that the count of the stack will be -- incremented after a push and therefore the stack will be non-empty. -- The item X is now the top of the stack. procedure Push(X : in Integer); --# global in out State; --# pre not Is_Full(State); --# post Count (State) = Count (State~) + 1 and --# Count (State) <= Max_Stack_Size and --# Stack_Entry (Count (State), State) = X; -- The precondition requires the stack is not empty when we -- pull a value from it. -- The postcondition indicates the stack count is decremented. procedure Pop (X : out Integer); --# global in out State; --# pre not Is_Empty (State); --# post Count (State) = Count (State~) - 1; -- Procedure that swaps the first two elements in a stack. procedure Swap2; --# global in out State; --# pre Count(State) >= 2; --# post Count(State) = Count(State~) and --# Stack_Entry (Count (State), State) = --# Stack_Entry (Count (State) - 1, State~) and --# Stack_Entry (Count (State) - 1, State) = --# Stack_Entry (Count (State), State~); -- Initializes the Stack. procedure Initialize; --# global out State; --# post Is_Empty (State); end Stack; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 package body Stack --# own State is My_Stack; is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; type Stack_Type is record S : Vector; Pointer : Pointer_Range; end record; Initial_Stack : constant Stack_Type := Stack_Type'(S => Vector'(others => 0), Pointer => 0); My_Stack : Stack_Type; procedure Push(X : in Integer) --# global in out My_Stack; --# pre My_Stack.Pointer < Stack_Size; is begin My_Stack.Pointer := My_Stack.Pointer + 1; My_Stack.S(My_Stack.Pointer) := X; end Push; procedure Pop (X : out Integer) --# global in out My_Stack; --# pre My_Stack.Pointer >= 1; is begin X := My_Stack.S (My_Stack.Pointer); My_Stack.Pointer := My_Stack.Pointer - 1; end Pop; procedure Swap2 --# global in out My_Stack; --# post My_Stack.Pointer = My_Stack~.Pointer; is Temp : Integer; begin Temp := My_Stack.S (1); My_Stack.S (1) := My_Stack.S (2); My_Stack.S (2) := Temp; end Swap2; procedure Initialize --# global out My_Stack; --# post My_Stack.Pointer = 0; is --# for Initial_Stack declare Rule; begin My_Stack := Initial_Stack; end Initialize; end Stack; 

Specification in SPARK 2014

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 package Stack with SPARK_Mode, Abstract_State => State, Initializes => State, Initial_Condition => Is_Empty is -- In SPARK 2014 we can specify an initial condition for the -- elaboration of a package and so initialization may be done -- during the elaboration of the package Stack, rendering the need -- for an initialization procedure unnecessary. -- Abstract states do not have types in SPARK 2014 they can only -- be directly referenced in Global and Depends aspects. -- Proof functions are actual functions but they may have the -- convention Ghost meaning that they can only be called from -- assertion expressions, e.g., pre and postconditions function Max_Stack_Size return Natural with Ghost; -- Returns the number of elements on the stack function Count return Natural with Global => (Input => State), Ghost; -- Returns the Nth entry on the stack. Stack_Entry (Count) is the -- top of stack function Stack_Entry (N : Natural) return Integer with Global => (Input => State), Pre => N in 1 .. Count, Ghost; -- A body (refined) version of this function can (must) be -- provided in the body of the package. function Is_Empty return Boolean is (Count = 0) with Global => State, Ghost; function Is_Full return Boolean is (Count = Max_Stack_Size) with Global => State, Ghost; -- The precondition requires the stack is not full when a value, -- X, is pushed onto it. Functions with global items (Is_Full -- with global State in this case) can be called in an assertion -- expression such as the precondition here. The postcondition -- indicates that the count of the stack will be incremented after -- a push and therefore the stack will be non-empty. The item X -- is now the top of the stack. procedure Push (X : in Integer) with Global => (In_Out => State), Pre => not Is_Full, Post => Count = Count'Old + 1 and Count <= Max_Stack_Size and Stack_Entry (Count) = X; -- The precondition requires the stack is not empty when we pull a -- value from it. The postcondition indicates the stack count is -- decremented. procedure Pop (X : out Integer) with Global => (In_Out => State), Pre => not Is_Empty, Post => Count = Count'Old - 1; -- Procedure that swaps the top two elements in a stack. procedure Swap2 with Global => (In_Out => State), Pre => Count >= 2, Post => Count = Count'Old and Stack_Entry (Count) = Stack_Entry (Count - 1)'Old and Stack_Entry (Count - 1) = Stack_Entry (Count)'Old; end Stack; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 package body Stack with SPARK_Mode, Refined_State => (State => My_Stack) is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1 .. Stack_Size; type Vector is array(Index_Range) of Integer; type Stack_Type is record S : Vector; Pointer : Pointer_Range; end record; Initial_Stack : constant Stack_Type := Stack_Type'(S => Vector'(others => 0), Pointer => 0); My_Stack : Stack_Type; function Max_Stack_Size return Natural is (Stack_Size); function Count return Natural is (Natural (My_Stack.Pointer)) with Refined_Global => My_Stack; function Stack_Entry (N : Natural) return Integer is (My_Stack.S (Index_Range (N))) with Refined_Global => My_Stack; procedure Push(X : in Integer) with Refined_Global => (In_Out => My_Stack) is begin My_Stack.Pointer := My_Stack.Pointer + 1; My_Stack.S(My_Stack.Pointer) := X; end Push; procedure Pop (X : out Integer) with Refined_Global => (In_Out => My_Stack) is begin X := My_Stack.S (My_Stack.Pointer); My_Stack.Pointer := My_Stack.Pointer - 1; end Pop; procedure Swap2 with Refined_Global => (In_Out => My_Stack) is Temp : Integer; begin Temp := My_Stack.S (My_Stack.Pointer); My_Stack.S (My_Stack.Pointer) := My_Stack.S (My_Stack.Pointer - 1); My_Stack.S (My_Stack.Pointer - 1) := Temp; end Swap2; begin My_Stack := Initial_Stack; end Stack; 

### 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 package Stack_External_Prover with SPARK_Mode, Abstract_State => State, Initializes => State, Initial_Condition => Is_Empty is -- A Ghost function may be an Import which means that no body is -- given in the SPARK 2014 code and the proof has to be discharged -- by an external prover. Of course, such functions are not -- executable. function Max_Stack_Size return Natural with Global => null, Ghost, Import; -- Returns the number of elements on the stack function Count return Natural with Global => (Input => State), Ghost, Import; -- Returns the Nth entry on the stack. Stack_Entry (Count) is the -- top of stack function Stack_Entry (N : Natural) return Integer with Global => (Input => State), Ghost, Import; function Is_Empty return Boolean with Global => State, Ghost, Import; function Is_Full return Boolean with Global => State, Ghost, Import; procedure Push (X : in Integer) with Global => (In_Out => State), Pre => not Is_Full, Post => Count = Count'Old + 1 and Count <= Max_Stack_Size and Stack_Entry (Count) = X; procedure Pop (X : out Integer) with Global => (In_Out => State), Pre => not Is_Empty, Post => Count = Count'Old - 1; procedure Swap2 with Global => (In_Out => State), Pre => Count >= 2, Post => Count = Count'Old and Stack_Entry (Count) = Stack_Entry (Count - 1)'Old and Stack_Entry (Count - 1) = Stack_Entry (Count)'Old; end Stack_External_Prover; 

### 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 Proof types and proof functions. 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 Proof types and proof functions 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 package Stack_Functional_Spec --# own State : Abstract_Stack; is -- It is not possible to specify that the stack will be -- initialized to empty except by having an initialization -- subprogram called during program execution (as opposed to -- package elaboration). -- Proof functions to indicate whether or not the Stack is empty -- and whether or not it is full. --# type Abstract_Stack is abstract; --# function Max_Stack_Size return Natural; -- Proof function to give the number of elements on the stack. --# function Count(Input : Abstract_Stack) return Natural; -- Proof function returns the Nth entry on the stack. -- Stack_Entry (Count (State)) is the top of stack --# function Stack_Entry (S : Abstract_Stack; N : Natural) return Integer; --# pre N in 1 .. Count (S); -- A refined version of this function cannot be written because -- the abstract view has a formal parameter of type Abstract_Stack -- whereas the refined view would not have this parameter but use -- a global. A user defined proof rule would be required to -- define this function. Alternatively, it could be written as an -- Ada function where the the global and formal parameter views -- would be available. However, the function would then be -- callable and generate implementation code. --# function Is_Empty(Input : Abstract_Stack) return Boolean; --# return Count (Input) = 0; --# function Is_Full(Input : Abstract_Stack) return Boolean; --# return Count (Input) = Max_Stack_Size; -- The precondition requires the stack is not full when a value, X, -- is pushed onto it. -- Functions with global items (Is_Full with global State in this case) -- can be called in an assertion expression such as the precondition here. -- The postcondition indicates that the count of the stack will be -- incremented after a push and therefore the stack will be non-empty. -- The item X is now the top of the stack and the contents of the rest of -- the stack are unchanged. procedure Push(X : in Integer); --# global in out State; --# pre not Is_Full(State); --# post Count (State) = Count (State~) + 1 and --# Count (State) <= Max_Stack_Size and --# Stack_Entry (State, Count (State)) = X and --# (for all I in Natural range 1 .. Count (State~) => --# (Stack_Entry (State, I) = Stack_Entry (State~, I))); -- The precondition requires the stack is not empty when we -- pull a value from it. -- The postcondition indicates that the X = the old top of stack, -- the stack count is decremented, and the contents of the stack excluding -- the old top of stack are unchanged. procedure Pop (X : out Integer); --# global in out State; --# pre not Is_Empty (State); --# post Count (State) = Count (State~) - 1 and --# X = Stack_Entry (State~, Count (State~)) and --# (for all I in Natural range 1 .. Count (State) => --# (Stack_Entry (State, I) = Stack_Entry (State~, I))); -- The precondition requires that the stack has at least 2 entries -- (Count >= 2). -- The postcondition states that the top two elements of the stack are -- transposed but the remainder of the stack is unchanged. procedure Swap2; --# global in out State; --# pre Count(State) >= 2; --# post Count(State) = Count(State~) and --# Stack_Entry (State, Count (State)) = --# Stack_Entry (State~, Count (State) - 1) and --# Stack_Entry (State, Count (State) - 1) = --# Stack_Entry (State~, Count (State)) and --# (for all I in Natural range 1 .. Count (State) => --# (Stack_Entry (State, I) = Stack_Entry (State~, I))); -- Initializes the Stack. procedure Initialize; --# global out State; --# post Is_Empty (State); end Stack_Functional_Spec; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 package body Stack_Functional_Spec --# own State is My_Stack; is Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1..Stack_Size; type Vector is array(Index_Range) of Integer; type Stack_Type is record S : Vector; Pointer : Pointer_Range; end record; Initial_Stack : constant Stack_Type := Stack_Type'(S => Vector'(others => 0), Pointer => 0); My_Stack : Stack_Type; procedure Push(X : in Integer) --# global in out My_Stack; --# pre My_Stack.Pointer < Stack_Size; is begin My_Stack.Pointer := My_Stack.Pointer + 1; My_Stack.S(My_Stack.Pointer) := X; end Push; procedure Pop (X : out Integer) --# global in out My_Stack; --# pre My_Stack.Pointer >= 1; is begin X := My_Stack.S (My_Stack.Pointer); My_Stack.Pointer := My_Stack.Pointer - 1; end Pop; procedure Swap2 --# global in out My_Stack; --# post My_Stack.Pointer = My_Stack~.Pointer; is Temp : Integer; begin Temp := My_Stack.S (1); My_Stack.S (1) := My_Stack.S (2); My_Stack.S (2) := Temp; end Swap2; procedure Initialize --# global out My_Stack; --# post My_Stack.Pointer = 0; is --# for Initial_Stack declare Rule; begin My_Stack := Initial_Stack; end Initialize; end Stack_Functional_Spec; 

Specification in SPARK 2014

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 pragma Unevaluated_Use_Of_Old(Allow); package Stack_Functional_Spec with SPARK_Mode, Abstract_State => State, Initializes => State, Initial_Condition => Is_Empty is -- Abstract states do not have types in SPARK 2014 but to provide -- functional specifications it is sometimes necessary to refer to -- the abstract state in an assertion expression such as a post -- condition. To do this in SPARK 2014 an Ada type declaration is -- required to represent the type of the abstract state, then a -- function applied to the abstract state (as a global) can be -- written which returns an object of the declared type. type Stack_Type is private; -- The Abstract_State name may be overloaded by the function which -- represents it in assertion expressions. function State return Stack_Type with Global => State; function Max_Stack_Size return Natural with Ghost; -- Returns the number of elements on the stack -- A function may have a formal parameter (or return a value) -- of the abstract state. function Count (S : Stack_Type) return Natural with Ghost; -- Returns the Nth entry on the stack. -- Stack_Entry (S, Count (S)) is the top of stack function Stack_Entry (S : Stack_Type; N : Natural) return Integer with Pre => N in 1 .. Count (S), Ghost; -- The ghost function Count can be called in the function -- expression because Is_Empty is also a ghost function. function Is_Empty return Boolean is (Count (State) = 0) with Global => State, Ghost; function Is_Full return Boolean is (Count(State) = Max_Stack_Size) with Global => State, Ghost; -- The precondition requires the stack is not full when a value, X, -- is pushed onto it. -- Functions with global items (Is_Full with global State in this case) -- can be called in an assertion expression such as the precondition here. -- The postcondition indicates that the count of the stack will be -- incremented after a push and therefore the stack will be non-empty. -- The item X is now the top of the stack and the contents of the rest of -- the stack are unchanged. procedure Push (X : in Integer) with Global => (In_Out => State), Pre => not Is_Full, Post => Count (State) = Count (State'Old) + 1 and Count (State) <= Max_Stack_Size and Stack_Entry (State, Count (State)) = X and (for all I in 1 .. Count (State'Old) => Stack_Entry (State, I) = Stack_Entry (State'Old, I)); -- The precondition requires the stack is not empty when we -- pull a value from it. -- The postcondition indicates that the X = the old top of stack, -- the stack count is decremented, and the contents of the stack excluding -- the old top of stack are unchanged. procedure Pop (X : out Integer) with Global => (In_Out => State), Pre => not Is_Empty, Post => Count (State) = Count (State'Old) - 1 and X = Stack_Entry (State'Old, Count (State'Old)) and (for all I in 1 .. Count (State) => Stack_Entry (State, I) = Stack_Entry (State'Old, I)); -- The precondition requires that the stack has at least 2 entries -- (Count >= 2). -- The postcondition states that the top two elements of the stack are -- transposed but the remainder of the stack is unchanged. procedure Swap2 with Global => (In_Out => State), Pre => Count (State) >= 2, Post => Count(State) = Count (State'Old) and Stack_Entry (State, Count (State)) = Stack_Entry (State'Old, Count (State) - 1) and Stack_Entry (State, Count (State) - 1) = Stack_Entry (State'Old, Count (State)) and (for all I in 1 .. Count (State) - 2 => Stack_Entry (State, I) = Stack_Entry (State'Old, I)); private -- The full type declarion used to represent the abstract state. Stack_Size : constant := 100; type Pointer_Range is range 0 .. Stack_Size; subtype Index_Range is Pointer_Range range 1 .. Stack_Size; type Vector is array(Index_Range) of Integer; type Stack_Type is record S : Vector; Pointer : Pointer_Range; end record; end Stack_Functional_Spec; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 package body Stack_Functional_Spec with SPARK_Mode, Refined_State => (State => My_Stack) is Initial_Stack : constant Stack_Type := Stack_Type'(S => Vector'(others => 0), Pointer => 0); -- In this example the type used to represent the state -- abstraction and the actual type used in the implementation are -- the same, but they need not be. For instance S and Pointer -- could have been declared as distinct objects rather than -- composed into a record. Where the type representing the -- abstract state and the implementation of that state are -- different the function representing the abstract state has to -- convert implementation representation into the abstract -- representation. For instance, if S and Pointer were distinct -- objects the function State would have to return (S => S, -- Pointer => Pointer). My_Stack : Stack_Type; -- No conversion necessary as the abstract and implementation type -- is the same. function State return Stack_Type is (My_Stack) with Refined_Global => My_Stack; function Max_Stack_Size return Natural is (Stack_Size); function Count (S : Stack_Type) return Natural is (Natural (S.Pointer)); function Stack_Entry (S : Stack_Type; N : Natural) return Integer is (S.S (Index_Range (N))); procedure Push(X : in Integer) with Refined_Global => (In_Out => My_Stack) is begin My_Stack.Pointer := My_Stack.Pointer + 1; My_Stack.S(My_Stack.Pointer) := X; end Push; procedure Pop (X : out Integer) with Refined_Global => (In_Out => My_Stack) is begin X := My_Stack.S (My_Stack.Pointer); My_Stack.Pointer := My_Stack.Pointer - 1; end Pop; procedure Swap2 with Refined_Global => (In_Out => My_Stack) is Temp : Integer; begin Temp := My_Stack.S (My_Stack.Pointer); My_Stack.S (My_Stack.Pointer) := My_Stack.S (My_Stack.Pointer - 1); My_Stack.S (My_Stack.Pointer - 1) := Temp; end Swap2; begin My_Stack := Initial_Stack; end Stack_Functional_Spec; 

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

## 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 package Update_Examples is type Rec is record X, Y : Integer; end record; type Index is range 1 ..3; type Arr is array (Index) of Integer; type Arr_2D is array (Index, Index) of Integer; type Nested_Rec is record A : Integer; B : Rec; C : Arr; D : Arr_2D; end record; type Nested_Arr is array (Index) of Nested_Rec; -- Simple record update procedure P1 (R : in out Rec); --# post R = R~ [X => 1]; -- Simple 1D array update procedure P2 (A : in out Arr); --# post A = A~ [1 => 2]; -- 2D array update procedure P3 (A2D : in out Arr_2D); --# post A2D = A2D~ [1, 1 => 1; --# 2, 2 => 2; --# 3, 3 => 3]; -- Nested record update procedure P4 (NR : in out Nested_Rec); --# post NR = NR~ [A => 1; --# B => NR~.B [X => 1]; --# C => NR~.C [1 => 5]]; -- Nested array update procedure P5 (NA : in out Nested_Arr); --# post NA = NA~ [1 => NA~ (1) [A => 1; --# D => NA~ (1).D [2, 2 => 0]]; --# 2 => NA~ (2) [B => NA~ (2).B [X => 2]]; --# 3 => NA~ (3) [C => NA~ (3).C [1 => 5]]]; end Update_Examples; 

Specification in SPARK 2014

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 package Update_Examples with SPARK_Mode is type Rec is record X, Y : Integer; end record; type Arr is array (1 .. 3) of Integer; type Nested_Rec is record A : Integer; B : Rec; C : Arr; end record; type Nested_Arr is array (1 .. 3) of Nested_Rec; -- Simple record update procedure P1 (R : in out Rec) with Post => R = (R'Old with delta X => 1); -- this is equivalent to: -- R = (X => 1, -- Y => R'Old.Y) -- Simple 1D array update procedure P2 (A : in out Arr) with Post => A = (A'Old with delta 1 => 2); -- this is equivalent to: -- A = (1 => 2, -- 2 => A'Old (2), -- 3 => A'Old (3)); -- Nested record update procedure P3 (NR : in out Nested_Rec) with Post => NR = (NR'Old with delta A => 1, B => (NR'Old.B with delta X => 1), C => (NR'Old.C with delta 1 => 5)); -- this is equivalent to: -- NR = (A => 1, -- B.X => 1, -- B.Y => NR'Old.B.Y, -- C (1) => 5, -- C (2) => NR'Old.C (2), -- C (3) => NR'Old.C (3)) -- Nested array update procedure P4 (NA : in out Nested_Arr) with Post => NA = (NA'Old with delta 1 => (NA'Old (1) with delta A => 1), 2 => (NA'Old (2) with delta B => (NA'Old (2).B with delta X => 2)), 3 => (NA'Old (3) with delta C => (NA'Old (3).C with delta 1 => 5))); -- this is equivalent to: -- NA = (1 => (A => 1, -- B => NA'Old (1).B, -- C => NA'Old (1).C), -- 2 => (B.X => 2, -- B.Y => NA'Old (2).B.Y, -- A => NA'Old (2).A, -- C => NA'Old (2).C), -- 3 => (C => (1 => 5, -- 2 => NA'Old (3).C (2), -- 3 => NA'Old (3).C (3)), -- A => NA'Old (3).A, -- B => NA'Old (3).B)); end Update_Examples; 

## 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:

  1 2 3 4 5 6 7 8 9 10 11 12 13 package Loop_Entry is subtype ElementType is Natural range 0..1000; subtype IndexType is Positive range 1..100; type ArrayType is array (IndexType) of ElementType; procedure Clear (A: in out ArrayType; L,U: in IndexType); --# derives A from A, L, U; --# post (for all N in IndexType range L..U => (A(N) = 0)) and --# (for all N in IndexType => ((NU) -> A(N) = A~(N))); end Loop_Entry; 

Body in SPARK 2005:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 package body Loop_Entry is procedure Clear (A: in out ArrayType; L,U: in IndexType) is begin for I in IndexType range L..U loop A(I) := 0; --# assert (for all N in IndexType range L..I => (A(N) = 0)) and --# (for all N in IndexType => ((NI) -> A(N) = A~(N))) and --# U = U% and L <= I; -- Note U = U% is required to show that the vaule of U does not change -- within the loop. end loop; end Clear; end Loop_Entry; 

Specification in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pragma SPARK_Mode (On); package Loop_Entry is subtype ElementType is Natural range 0..1000; subtype IndexType is Positive range 1..100; type ArrayType is array (IndexType) of ElementType; procedure Clear (A: in out ArrayType; L,U: in IndexType) with Depends => (A => (A, L, U)), Post => (for all N in L..U => A(N) = 0) and (for all N in IndexType => (if NU then A(N) = A'Old(N))); end Loop_Entry; 

Body in SPARK 2014:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 pragma SPARK_Mode (On); package body Loop_Entry is procedure Clear (A: in out ArrayType; L,U: in IndexType) is begin for I in IndexType range L..U loop A(I) := 0; pragma Loop_Invariant ((for all N in L..I => (A(N) = 0)) and (for all N in IndexType => (if N < L or N > I then A(N) = A'Loop_Entry(N)))); -- Note it is not necessary to show that the vaule of U does not change -- within the loop. -- However 'Loop_Entry must be used rather than 'Old. end loop; end Clear; end Loop_Entry;