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

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

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

body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

Package patterns

Abstract Data Types (ADTs)

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:

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

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Specification of private child A in SPARK 2005:

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

Specification of private child B in SPARK 2005:

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

Specification of public child A in SPARK 2005:

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

Specification of public child B in SPARK 2005:

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

Body of parent in SPARK 2005:

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

Body of public child A in SPARK 2005:

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

Body of public child B in SPARK 2005:

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

Body of private child B in SPARK 2005:

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

Specification of parent in SPARK 2014:

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

Specification of private child A in SPARK 2014:

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

Specification of private child B in SPARK 2014:

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

Specification of public child A in SPARK 2014:

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

Specification of public child B in SPARK 2014:

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

Body of parent in SPARK 2014:

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

Body of public child A in SPARK 2014:

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

Body of public child B in SPARK 2014:

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

Body of private child B in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2014:

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

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2014:

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

Body of Parent in SPARK 2005:

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

Specifications of Private Children in SPARK 2005:

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

Bodies of Private Children in SPARK 2005:

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

Specification of Parent in SPARK 2014:

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

Body of Parent in SPARK 2014:

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

Specifications of Private Children in SPARK 2014:

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

Bodies of Private Children in SPARK 2014:

 1package body Power_14.Source_A_14
 2  with SPARK_Mode,
 3       Refined_State => (State => S)
 4is
 5   S : Integer := 0;
 6
 7   procedure Read (Level : out Integer)
 8     with Refined_Global  => (Input => S),
 9          Refined_Depends => (Level => S)
10   is
11   begin
12      Level := S;
13   end Read;
14end Power_14.Source_A_14;
 1package body Power_14.Source_B_14
 2  with SPARK_Mode,
 3       Refined_State => (State => S)
 4is
 5   S : Integer := 0;
 6
 7   procedure Read (Level : out Integer)
 8     with Refined_Global  => (Input => S),
 9          Refined_Depends => (Level => S)
10   is
11   begin
12      Level := S;
13   end Read;
14end 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-- Use of embedded packages to encapsulate state
2package Power_05
3--# own State;
4is
5   procedure Read_Power(Level : out Integer);
6   --# global State;
7   --# derives Level from State;
8end Power_05;

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Specification of input port in SPARK 2005:

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

Body of input port in SPARK 2005:

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

Specification of output port in SPARK 2005:

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

Body of output port in SPARK 2005:

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

Specification of main program in SPARK 2014:

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

Specification of input port in SPARK 2014:

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

Specification of output port in SPARK 2014:

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

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

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Component Switch specifications in SPARK 2005:

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

Switch body in SPARK 2005:

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

Abstract Switch specification in SPARK 2014:

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

Component Switch specifications in SPARK 2014:

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

Switch body in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Specifications in SPARK 2014:

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

Package nested inside package

See section Private, abstract state, refining onto concrete state of embedded package.

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:

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

Component Switch specifications in SPARK 2005:

As in Refinement of external state - voting input switch

Switch body in SPARK 2005:

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

Abstract Switch specification in SPARK 2014:

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

Component Switch specification in SPARK 2014:

As in Refinement of external state - voting input switch

Switch body in SPARK 2014:

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

Instead of the elaboration restrictions of SPARK 2005 a set of rules is applied in SPARK 2014 which determines when elaboration order control pragmas such as Elaborate_Body or Elaborate_All are required. These rules ensure the absence of elaboration order dependencies.

Examples of the features of SPARK 2014 elaboration order rules are given below. In the example described below the partial elaboration order would be either of P_14 or Q_14 specifications first followed by P_14 body because of the Elaborate_All on the specification of R_14 specification and the body of Q_14, then the elaboration of Q_14 body or the specification of R_14 and the body of R_14 after the elaboration of Q_14. Elaboration order dependencies are avoided by the (required) use of elaboration control pragmas.

Package Specifications in SPARK 2014:

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

Package Bodies in SPARK 2014

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

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

Body for Assume annotation in SPARK 2005:

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

Specification for Assume annotation in SPARK 2014:

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

Body for Assume annotation in SPARK 2014:

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

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

Body for Check annotation in SPARK 2005:

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

Specification for Check annotation in SPARK 2014:

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

Body for Check annotation in SPARK 2014:

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014

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

Body in SPARK 2014:

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

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014

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

Body in SPARK 2014:

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

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

Specification in SPARK 2014

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

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

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