SPARK 2005 to SPARK 2014 Mapping Specification

This appendix defines the mapping between SPARK 2005 and SPARK 2014. It is intended as both a completeness check for the SPARK 2014 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 2014 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 ‘Update attribute 4.4.1 A.6

Subprogram patterns

Global and Derives

This example demonstrates how global variables can be accessed through procedures/functions and presents how the SPARK 2005 derives annotation maps over to depends in SPARK 2014. The example consists of one procedure (Swap) and one function (Add). Swap accesses two global variables and swaps their contents while Add returns their sum.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
package Swap_Add_05
--# own X, Y: Integer;
is
   X, Y: Integer;

   procedure Swap;
   --# global in out X, Y;
   --# derives X from Y &
   --#         Y from X;

   function Add return Integer;
   --# global in X, Y;

end Swap_Add_05;

body in SPARK 2005:

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

   function Add return Integer
   is
   begin
      return X + Y;
   end Add;

end Swap_Add_05;

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
package Swap_Add_14
  with SPARK_Mode
is
   -- Visible variables are not state abstractions.
   X, Y: Integer;

   procedure Swap
     with Global  => (In_Out => (X, Y)),
          Depends => (X => Y,   -- to be read as "X depends on Y"
                      Y => X);  -- to be read as "Y depends on X"

   function Add return Integer
     with Global  => (Input => (X, Y));
end Swap_Add_14;

Body in SPARK 2014:

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

   function Add return Integer is (X + Y);
end Swap_Add_14;

Pre/Post/Return contracts

This example demonstrates how the Pre/Post/Return contracts are restructured and how they map from SPARK 2005 to SPARK 2014. Procedure Swap and function Add perform the same task as in the previous example, but the global variables have been replaced by parameters (this is not necessarry for proof) and they have been augmented by pre and post annotations. Two additional functions (Max and Divide) and one additional procedure (Swap_Array_Elements) have also been included in this example in order to demonstrate further features. Max returns the maximum of the two parameters. Divide returns the division of the two parameters after having ensured that the divisor is not equal to zero. The Swap_Array_Elements procedure swaps the contents of two elements of an array.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
package Swap_Add_Max_05 is

   subtype Index      is Integer range 1..100;
   type    Array_Type is array (Index) of Integer;

   procedure Swap (X , Y : in out Integer);
   --# post X = Y~ and Y = X~;

   function Add (X, Y : Integer) return Integer;
   --# pre ((X >= 0 and Y >= 0) -> (X + Y <= Integer'Last)) and
   --#     ((X <  0 and Y <  0) -> (X + Y >= Integer'First));
   --# return X + Y;

   function Max (X, Y : Integer) return Integer;
   --# return Z => (X >= Y -> Z = X) and
   --#             (Y >  X -> Z = Y);

   function Divide (X , Y : Integer) return Integer;
   --# pre Y /= 0 and X > Integer'First;
   --# return X / Y;

   procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type);
   --# post A = A~[I => A~(J); J => A~(I)];

end Swap_Add_Max_05;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
package body Swap_Add_Max_05
is
   procedure Swap (X, Y: in out Integer)
   is
      Temporary: Integer;
   begin
      Temporary := X;
      X         := Y;
      Y         := Temporary;
   end Swap;

   function Add (X, Y : Integer) return Integer
   is
   begin
      return X + Y;
   end Add;

   function Max (X, Y : Integer) return Integer
   is
      Result: Integer;
   begin
      if X >= Y then
         Result := X;
      else
         Result := Y;
      end if;
      return Result;
   end Max;

   function Divide (X, Y : Integer) return Integer
   is
   begin
      return X / Y;
   end Divide;

   procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type)
   is
      Temporary: Integer;
   begin
      Temporary := A(I);
      A(I)      := A(J);
      A(J)      := Temporary;
   end Swap_Array_Elements;

end Swap_Add_Max_05;

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
package Swap_Add_Max_14
  with SPARK_Mode
is
   subtype Index      is Integer range 1..100;
   type    Array_Type is array (Index) of Integer;

   procedure Swap (X, Y : in out Integer)
     with Post => (X = Y'Old and Y = X'Old);

   function Add (X, Y : Integer) return Integer
     with Pre  => (if X >= 0 and Y >= 0 then X <= Integer'Last - Y
                   elsif X < 0 and Y < 0 then X >= Integer'First - Y),
          -- The precondition may be written as X + Y in Integer if
          -- an extended arithmetic mode is selected
          Post => Add'Result = X + Y;

   function Max (X, Y : Integer) return Integer
     with Post => Max'Result = (if X >= Y then X else Y);

   function Divide (X, Y : Integer) return Integer
     with Pre  => Y /= 0 and X > Integer'First,
          Post => Divide'Result = X / Y;

   procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type)
     with Post => A = A'Old'Update (I => A'Old (J),
                                    J => A'Old (I));
end Swap_Add_Max_14;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
package body Swap_Add_Max_14
  with SPARK_Mode
is
   procedure Swap (X, Y : in out Integer) is
      Temporary: Integer;
   begin
      Temporary := X;
      X         := Y;
      Y         := Temporary;
   end Swap;

   function Add (X, Y : Integer) return Integer is (X + Y);

   function Max (X, Y : Integer) return Integer is
     (if X >= Y then X
      else Y);

   function Divide (X, Y : Integer) return Integer is (X / Y);

   procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type) is
      Temporary: Integer;
   begin
      Temporary := A(I);
      A(I)      := A(J);
      A(J)      := Temporary;
   end Swap_Array_Elements;
end Swap_Add_Max_14;

Attributes of unconstrained out parameter in precondition

The following example illustrates the fact that the attributes of an unconstrained formal array parameter of mode “out” are permitted to appear in a precondition. The flow analyzer also needs to be smart about this, since it knows that X’First and X’Last are well-defined in the body, even though the content of X is not.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
package P
is
   type A is array (Positive range <>) of Integer;

   -- Shows that X'First and X'Last _can_ be used in
   -- precondition here, even though X is mode "out"...
   procedure Init (X : out A);
   --# pre X'First = 1  and
   --#     X'Last  >= 20;
   --# post for all I in Positive range X'Range =>
   --#      ((I /= 20 -> (X (I) = 0)) and
   --#         (I = 1 -> (X (I) = X'Last)) and
   --#         (I = 20 -> (X (I) = -1)));

end P;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
package body P is

   procedure Init (X : out A) is
   begin
      X := (others => 0);
      X (1) := X'Last;
      X (20) := -1;
  end Init;

end P;

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
package P
  with SPARK_Mode
is
   type A is array (Positive range <>) of Integer;

   -- Shows that X'First, X'Last and X'Length _can_ be used
   -- in precondition here, even though X is mode "out"...
   procedure Init (X : out A)
     with Pre  => X'First = 1 and X'Last >= 20,
          Post => (for all I in X'Range =>
                     (if I = 1 then X (I) = X'Last
                      elsif I = 20 then X (I) = -1
                      else X (I) = 0));
end P;

Body in SPARK 2014:

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

Data Abstraction, Refinement and Initialization

This example demonstrates data abstraction and refinement. It also shows how abstract data is shown to be initialized during package elaboration (it need not be - it could be initialized through an explicit subprogram call, in which case the Initalizes annotation should not be given). There is also a demonstration of how procedures and functions can be nested within other procedures and functions. Furthermore, it illustrates how global variable refinement can be performed.

Specification in SPARK 2005:

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

Body in SPARK 2005:

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

Specification in SPARK 2014:

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

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
package body Nesting_Refinement_14
  -- State is refined onto two concrete variables X and Y
  with SPARK_Mode,
       Refined_State => (State => (X, Y))
is
   X, Y: Integer;

   procedure Operate_On_State
     with Refined_Global => (In_Out => X,
                             Output => Y)
   is
      Z: Integer;

      procedure Add_Z_To_X
        with Global => (In_Out => X,
                        Input  => Z)
      is
      begin
         X := X + Z;
      end Add_Z_To_X;

      procedure Overwrite_Y_With_Z
        with Global => (Output => Y,
                        Input  => Z)
      is
      begin
         Y := Z;
      end Overwrite_Y_With_Z;
   begin
      Z := 5;
      Add_Z_To_X;
      Overwrite_Y_With_Z;
   end Operate_On_State;

begin
   -- Promised to initialize State
   -- (which consists of X and Y)
   X := 10;
   Y := 20;
end Nesting_Refinement_14;

Package patterns

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:

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

   procedure Clear(S : out Stack);
   procedure Push(S : in out Stack; X : in Integer);
   procedure Pop(S : in out Stack; X : out Integer);
end Stacks_05;

Private type

Similarly to the previous example, this one does not contain any annotations either. Due to this, the SPARK 2005 and SPARK 2014 versions are exactly the same. Only the specification of the 2005 version shall be presented.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
package Stacks_05 is

   type Stack is private;

   function Is_Empty(S : Stack) return Boolean;
   function Is_Full(S : Stack) return Boolean;

   procedure Clear(S : out Stack);
   procedure Push(S : in out Stack; X : in Integer);
   procedure Pop(S : in out Stack; X : out Integer);

private
   Stack_Size : constant := 100;
   type Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
   type Vector is array(Index_Range) of Integer;

   type Stack is
      record
         Stack_Vector : Vector;
         Stack_Pointer : Pointer_Range;
      end record;
end Stacks_05;

Private type with pre/post contracts

This example demonstrates how pre and post conditions of subprograms may be specified in terms of functions declared in the same package specification. The function declarations are completed in the body and the postconditions of the completed functions are used to prove the implementations of the other subprograms. In SPARK 2014 explicit postconditions do not have to be specified on the bodies of the functions as they are implemented as expression functions and the expression, E, of the function acts as a default refined postcondition, i.e., F’Result = E. Note that the SPARK 2014 version is proven entirely automatically whereas the SPARK 2005 version requires user defined proof rules.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
package Stacks_05
is
   
   type Stack is private;

   function Is_Empty(S : Stack) return Boolean;
   function Is_Full(S : Stack) return Boolean;
      
   procedure Clear(S : in out Stack);
   --# post Is_Empty(S);
   procedure Push(S : in out Stack; X : in Integer);
   --# pre  not Is_Full(S);
   --# post not Is_Empty(S);
   procedure Pop(S : in out Stack; X : out Integer);
   --# pre  not Is_Empty(S);
   --# post not Is_Full(S);

private
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1 .. Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   type Stack is
      record
         Stack_Vector  : Vector;
         Stack_Pointer : Pointer_Range;
      end record;
end Stacks_05;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
package body Stacks_05 is

   function Is_Empty (S : Stack) return Boolean
   --# return S.Stack_Pointer = 0;
   is
   begin
      return S.Stack_Pointer = 0;
   end Is_Empty;

   function Is_Full (S : Stack) return Boolean
   --# return S.Stack_Pointer = Stack_Size;
   is
   begin
      return S.Stack_Pointer = Stack_Size;
   end Is_Full;

   procedure Clear (S : in out Stack)
   --# post Is_Empty(S);
   is
   begin
      S.Stack_Pointer := 0;
   end Clear;

   procedure Push (S : in out Stack; X : in Integer)
   is
   begin
      S.Stack_Pointer := S.Stack_Pointer + 1;
      S.Stack_Vector (S.Stack_Pointer) := X;
   end Push;

   procedure Pop (S : in out Stack; X : out Integer)
   is
   begin
      X := S.Stack_Vector (S.Stack_Pointer);
      S.Stack_Pointer := S.Stack_Pointer - 1;
   end Pop;
end Stacks_05;

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
package Stacks_14
  with SPARK_Mode
is
   type Stack is private;

   function Is_Empty(S : Stack) return Boolean;
   function Is_Full(S : Stack) return Boolean;

   procedure Clear(S : in out Stack)
     with Post => Is_Empty(S);

   procedure Push(S : in out Stack; X : in Integer)
     with Pre  => not Is_Full(S),
          Post => not Is_Empty(S);

   procedure Pop(S : in out Stack; X : out Integer)
     with Pre  => not Is_Empty(S),
          Post => not Is_Full(S);

private
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1 .. Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   type Stack is record
      Stack_Vector  : Vector;
      Stack_Pointer : Pointer_Range;
   end record;
end Stacks_14;

Body in SPARK 2014:

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

   -- Expression function has default refined postcondition of
   -- Is_Empty'Result = (S.Stack_Pointer = Stack_Size)
   function Is_Full(S : Stack) return Boolean is (S.Stack_Pointer = Stack_Size);

   procedure Clear(S : in out Stack) is
   begin
      S.Stack_Pointer := 0;
   end Clear;

   procedure Push(S : in out Stack; X : in Integer) is
   begin
      S.Stack_Pointer := S.Stack_Pointer + 1;
      S.Stack_Vector(S.Stack_Pointer) := X;
   end Push;

   procedure Pop(S : in out Stack; X : out Integer) is
   begin
      X := S.Stack_Vector(S.Stack_Pointer);
      S.Stack_Pointer := S.Stack_Pointer - 1;
   end Pop;
end Stacks_14;

Private/Public child visibility

The following example demonstrates visibility rules that apply between public children, private children and their parent in SPARK 2005. More specifically, it shows that:

  • Private children are able to see their private siblings but not their public siblings.
  • Public children are able to see their public siblings but not their private siblings.
  • All children have access to their parent but the parent can only access private children.

Applying the SPARK tools on the following files will produce certain errors. This was intentionally done in order to illustrate both legal and illegal access attempts.

SPARK 2014 shares Ada2012’s visibility rules. No restrictions have been applied in terms of visibility. Note that SPARK 2014 code does not require Inherit annotations.

Specification of parent in SPARK 2005:

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

Specification of private child A in SPARK 2005:

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

Specification of private child B in SPARK 2005:

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

Specification of public child A in SPARK 2005:

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

Specification of public child B in SPARK 2005:

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

Body of parent in SPARK 2005:

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

   function G (X : Integer) return Integer is
   begin
      return Public_Child_A_05.G (X);
   end G;

end Parent_05;

Body of public child A in SPARK 2005:

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

Body of public child B in SPARK 2005:

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

Body of private child B in SPARK 2005:

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

Specification of parent in SPARK 2014:

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

Specification of private child A in SPARK 2014:

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

Specification of private child B in SPARK 2014:

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

Specification of public child A in SPARK 2014:

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

Specification of public child B in SPARK 2014:

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

Body of parent in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
with Parent_14.Private_Child_A_14,   -- OK
     Parent_14.Public_Child_A_14;    -- OK

package body Parent_14
  with SPARK_Mode
is
   function F (X : Integer) return Integer is (Private_Child_A_14.F (X));

   function G (X : Integer) return Integer is (Public_Child_A_14.G (X));
end Parent_14;

Body of public child A in SPARK 2014:

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

Body of public child B in SPARK 2014:

1
2
3
4
5
6
7
8
with Parent_14.Private_Child_B_14;

package body Parent_14.Public_Child_B_14
  with SPARK_Mode
is
   function H (X : Integer) return Integer is
     (Parent_14.Private_Child_B_14.H (X));
end Parent_14.Public_Child_B_14;

Body of private child B in SPARK 2014:

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

Abstract State Machines (ASMs)

Visible, concrete state

Initialized by declaration

The example that follows presents a way in SPARK 2005 of initializing a concrete own variable (a state that is not refined) at the point of the declaration of the variables that compose it. Generally it is not good practice to declare several concrete own variables, data abstraction should be used but here we are doing it for the point of illustration.

In SPARK 2014 the client’s view of package state is either visible (declared in the visible part of the package) or a state abstraction representing hidden state. A variable cannot overload the name of a state abstraction and therefore a state abstraction must be completed by a refinement given in the body of the package - there is no concept of a concrete state abstraction. The constituents of a state abstraction may be initialized at their declaration.

Specification in SPARK 2005:

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

   procedure Pop(X : out Integer);
   --# global in S; in out Pointer;
end Stack_05;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
package body Stack_05
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S : Vector := Vector'(Index_Range => 0);  -- Initialization of S
   Pointer : Pointer_Range := 0;             -- Initialization of Pointer

   procedure Push(X : in Integer) 
   is
   begin
      Pointer := Pointer + 1;
      S(Pointer) := X;
   end Push;

   procedure Pop(X : out Integer) 
   is
   begin
      X := S(Pointer);
      Pointer := Pointer - 1;
   end Pop;

end Stack_05;

Specification in SPARK 2014:

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

   procedure Pop(X : out Integer)
     with Global => (Input  => S_State,
                     In_Out => Pointer_State);
end Stack_14;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
package body Stack_14
  with SPARK_Mode,
       Refined_State => (S_State       => S,
                         Pointer_State => Pointer)
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S : Vector := Vector'(Index_Range => 0);  -- Initialization of S
   Pointer : Pointer_Range := 0;             -- Initialization of Pointer

   procedure Push (X : in Integer)
     with Refined_Global => (In_Out => (S, Pointer))
   is
   begin
      Pointer := Pointer + 1;
      S (Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
     with Refined_Global => (Input  => S,
                             In_Out => Pointer)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;
end Stack_14;
Initialized by elaboration

The following example presents how a package’s concrete state can be initialized at the statements section of the body. The specifications of both SPARK 2005 and SPARK 2014 are not presented since they are identical to the specifications of the previous example.

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
package body Stack_05
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S : Vector;
   Pointer : Pointer_Range;

   procedure Push(X : in Integer)
   is
   begin
      Pointer := Pointer + 1;
      S(Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
   is
   begin
      X := S(Pointer);
      Pointer := Pointer - 1;
   end Pop;

begin  -- initialization
   Pointer := 0;
   S := Vector'(Index_Range => 0);
end Stack_05;

Body in SPARK 2014:

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

   S : Vector;
   Pointer : Pointer_Range;

   procedure Push (X : in Integer)
     with Refined_Global => (In_Out => (S, Pointer))
   is
   begin
      Pointer := Pointer + 1;
      S (Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
     with Refined_Global => (Input  => S,
                             In_Out => Pointer)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;
begin
   -- initialization
   Pointer := 0;
   S := Vector'(Index_Range => 0);
end Stack_14;

Private, concrete state

In SPARK 2005 variables declared in the private part of a package are considered to be concrete own variables. In SPARK 2014 they are hidden state and must be constituents of a state abstraction.

The SPARK 2005 body has not been included since it does not contain any annotations.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
package Stack_05
--# own S, Pointer;
is
   procedure Push(X : in Integer);
   --# global in out S, Pointer;

   procedure Pop(X : out Integer);
   --# global in     S;
   --#        in out Pointer;
private
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S : Vector;
   Pointer : Pointer_Range;
end Stack_05;

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
package Stack_14
  with SPARK_Mode,
       Abstract_State => (S_State, Pointer_State)
is
   procedure Push(X : in Integer)
     with Global => (In_Out => (S_State, Pointer_State));

   procedure Pop(X : out Integer)
     with Global => (Input  => S_State,
                     In_Out => Pointer_State);

private
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S       : Vector with Part_Of => S_State;
   Pointer : Pointer_Range with Part_Of => Pointer_State;
end Stack_14;

Body in SPARK 2014:

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

   procedure Pop (X : out Integer)
     with Refined_Global => (Input  => S,
                             In_Out => Pointer)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;
end Stack_14;

Private, abstract state, refining onto concrete states in body

Initialized by procedure call

In this example, the abstract state declared at the specification is refined at the body. Procedure Init can be invoked by users of the package, in order to initialize the state.

Specification in SPARK 2005:

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

   procedure Pop(X : out Integer);
   --# global in out State;

   procedure Init;
   --# global    out State;

end Stack_05;

Body in SPARK 2005:

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

   Pointer : Pointer_Range;
   S       : Vector;

   procedure Push(X : in Integer)
   --# global in out Pointer, S;
   is
   begin
      Pointer := Pointer + 1;
      S(Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
   --# global in     S;
   --#        in out Pointer;
   is
   begin
      X := S(Pointer);
      Pointer := Pointer - 1;
   end Pop;

   procedure Init
   --# global    out Pointer, S;
   is
   begin
      Pointer := 0;
      S := Vector'(Index_Range => 0);
   end Init;
end Stack_05;

Specification in SPARK 2014:

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

   procedure Pop(X : out Integer)
     with Global => (In_Out => State);

   procedure Init
     with Global => (Output => State);
end Stack_14;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
package body Stack_14
  with SPARK_Mode,
       Refined_State => (State => (Pointer, S))
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   Pointer : Pointer_Range;
   S       : Vector;

   procedure Push(X : in Integer)
     with Refined_Global => (In_Out => (Pointer, S))
   is
   begin
      Pointer := Pointer + 1;
      S (Pointer) := X;
   end Push;

   procedure Pop (X : out Integer)
     with Refined_Global => (In_Out => Pointer,
                             Input  => S)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;

   procedure Init
     with Refined_Global => (Output => (Pointer, S))
   is
   begin
      Pointer := 0;
      S := (Index_Range => 0);
   end Init;
end Stack_14;
Initialized by elaboration of declaration

The example that follows introduces an abstract state at the specification and refines it at the body. The constituents of the abstract state are initialized at declaration.

Specification in SPARK 2005:

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

   procedure Pop(X : out Integer);
   --# global in out State;

end Stack_05;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
package body Stack_05
--# own State is Pointer, S; -- refinement of state
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S : Vector := Vector'(others => 0);
   Pointer : Pointer_Range := 0;
   -- initialization by elaboration of declaration

   procedure Push(X : in Integer)
   --# global in out Pointer, S;
   is
   begin
      Pointer := Pointer + 1;
      S(Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
   --# global in     S;
   --#        in out Pointer;
   is
   begin
      X := S(Pointer);
      Pointer := Pointer - 1;
   end Pop;
end Stack_05;

Specification in SPARK 2014:

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

   procedure Pop(X : out Integer)
     with Global => (In_Out => State);
end Stack_14;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
package body Stack_14
  with SPARK_Mode,
       Refined_State => (State => (Pointer, S)) -- refinement of state
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S : Vector := (others => 0);
   Pointer : Pointer_Range := 0;
   -- initialization by elaboration of declaration

   procedure Push(X : in Integer)
     with Refined_Global => (In_Out => (Pointer, S))
   is
   begin
      Pointer := Pointer + 1;
      S (Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
     with Refined_Global => (In_Out => Pointer,
                             Input  => S)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;
end Stack_14;
Initialized by package body statements

This example introduces an abstract state at the specification and refines it at the body. The constituents of the abstract state are initialized at the statements part of the body. The specifications of the SPARK 2005 and SPARK 2014 versions of the code are as in the previous example and have thus not been included.

Body in SPARK 2005:

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

   S : Vector;
   Pointer : Pointer_Range;

   procedure Push(X : in Integer)
   --# global in out Pointer, S;
   is
   begin
      Pointer := Pointer + 1;
      S(Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
   --# global in out Pointer;
   --#        in     S;
   is
   begin
      X := S(Pointer);
      Pointer := Pointer - 1;
   end Pop;
begin  -- initialized by package body statements
   Pointer := 0;
   S := Vector'(Index_Range => 0);
end Stack_05;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
package body Stack_14
  with SPARK_Mode,
       Refined_State => (State => (Pointer, S))  -- refinement of state
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S       : Vector;
   Pointer : Pointer_Range;

   procedure Push(X : in Integer)
     with Refined_Global => (In_Out => (Pointer, S))
   is
   begin
      Pointer := Pointer + 1;
      S (Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
     with Refined_Global => (In_Out => Pointer,
                             Input  => S)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;
begin
   -- initialized by package body statements
   Pointer := 0;
   S := (Index_Range => 0);
end Stack_14;
Initialized by mixture of declaration and statements

This example introduces an abstract state at the specification and refines it at the body. Some of the constituents of the abstract state are initialized during their declaration and the rest at the statements part of the body.

Specification in SPARK 2005:

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

   procedure Pop(X : out Integer);
   --# global in out Stack;

end Stack_05;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
package body Stack_05
--# own Stack is S, Pointer; -- state refinement
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;
   S : Vector;

   Pointer : Pointer_Range := 0;
   -- initialization by elaboration of declaration

   procedure Push(X : in Integer)
   --# global in out S, Pointer;
   is
   begin
      Pointer := Pointer + 1;
      S(Pointer) := X;
   end Push;

   procedure Pop(X : out Integer)
   --# global in     S;
   --#        in out Pointer;
   is
   begin
      X := S(Pointer);
      Pointer := Pointer - 1;
   end Pop;
begin  -- initialization by body statements
   S := Vector'(Index_Range => 0);
end Stack_05;

Specification in SPARK 2014:

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

   procedure Pop(X : out Integer)
     with Global => (In_Out => Stack);
end Stack_14;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
package body Stack_14
  with SPARK_Mode,
       Refined_State => (Stack => (S, Pointer)) -- state refinement
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   S       : Vector; -- left uninitialized
   Pointer : Pointer_Range := 0;
   -- initialization by elaboration of declaration

   procedure Push(X : in Integer)
     with Refined_Global => (In_Out => (S, Pointer))
   is
   begin
      Pointer := Pointer + 1;
      S (Pointer) := X;
   end Push;

   procedure Pop (X : out Integer)
     with Refined_Global => (Input  => S,
                             In_Out => Pointer)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;
begin
   -- partial initialization by body statements
   S := (Index_Range => 0);
end Stack_14;

Initial condition

This example introduces a new SPARK 2014 feature that did not exist in SPARK 2005. On top of declaring an abstract state and promising to initialize it, we also illustrate certain conditions that will be valid after initialization. There is a verification condition to show that immediately after the elaboration of the package that the specified Initial_Condition is True. Checks will be generated that have to be proven (or executed at run-time) to show that the initial condition is True.

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
package Stack_14
  with SPARK_Mode,
       Abstract_State    => State,
       Initializes       => State,
       Initial_Condition => Is_Empty  -- Stating that Is_Empty holds
                                      -- after initialization
is
   function Is_Empty return Boolean
     with Global => State;

   function Is_Full return Boolean
     with Global => State;

   function Top return Integer
     with Global => State,
          Pre    => not Is_Empty;

   procedure Push (X: in Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Full,
          Post   => Top = X;

   procedure Pop (X: out Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Empty;
end Stack_14;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
package body Stack_14
  with SPARK_Mode,
       Refined_State => (State => (S,
                                   Pointer)) -- State refinement
is
   Max_Stack_Size : constant := 1024;
   type Pointer_Range is range 0 .. Max_Stack_Size;
   subtype Index_Range is Pointer_Range range 1 .. Max_Stack_Size;
   type Vector is array (Index_Range) of Integer;

   -- Declaration of constituents
   S       : Vector;
   Pointer : Pointer_Range;

   -- The subprogram contracts are refined in terms of the constituents.
   -- Expression functions could be used where applicable

   function Is_Empty  return Boolean is (Pointer = 0)
     with Refined_Global => Pointer;

   function Is_Full  return Boolean is (Pointer = Max_Stack_Size)
     with Refined_Global => Pointer;

   function Top return Integer is (S (Pointer))
     with Refined_Global => (Pointer, S);

   procedure Push(X: in Integer)
     with Refined_Global => (In_Out => (Pointer, S))
   is
   begin
      Pointer := Pointer + 1;
      S (Pointer) := X;
   end Push;

   procedure Pop(X: out Integer)
     with Refined_Global => (Input  => S,
                             In_Out => Pointer)
   is
   begin
      X := S (Pointer);
      Pointer := Pointer - 1;
   end Pop;
begin
   -- Initialization - we promised to initialize the state
   -- and that initially the stack will be empty
   Pointer := 0;  -- Is_Empty is True.
   S := Vector'(Index_Range => 0);
end Stack_14;

Private, abstract state, refining onto state of private child

The following example shows a parent package Power that contains an own variable (a state abstraction). This state abstraction is refined onto state abstractions of two private children Source_A and Source_B.

Specification of Parent in SPARK 2005:

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

Body of Parent in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
with Power_05.Source_A_05, Power_05.Source_B_05;

package body Power_05
--# own State is Power_05.Source_A_05.State,
--#              Power_05.Source_B_05.State;
is

  procedure Read_Power(Level : out Integer)
  --# global Source_A_05.State, Source_B_05.State;
  --# derives
  --#     Level
  --#     from
  --#         Source_A_05.State,
  --#         Source_B_05.State;
  is
     Level_A : Integer;
     Level_B : Integer;
  begin
     Source_A_05.Read (Level_A);
     Source_B_05.Read (Level_B);
     Level := Level_A + Level_B;
  end Read_Power;

end Power_05;

Specifications of Private Children in SPARK 2005:

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

Bodies of Private Children in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
package body Power_05.Source_A_05
--# own State is S;
is
   S : Integer := 0;

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

   procedure Read (Level : out Integer)
   --# global in S;
   --# derives Level from S;
   is
   begin
      Level := S;
   end Read;
end Power_05.Source_B_05;

Specification of Parent in SPARK 2014:

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

Body of Parent in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
with Power_14.Source_A_14,
     Power_14.Source_B_14;

package body Power_14
  with SPARK_Mode,
       Refined_State => (State => (Power_14.Source_A_14.State,
                                   Power_14.Source_B_14.State))
is
   procedure Read_Power(Level : out Integer)
     with Refined_Global  => (Source_A_14.State, Source_B_14.State),
          Refined_Depends => (Level => (Source_A_14.State,
                                        Source_B_14.State))
   is
      Level_A : Integer;
      Level_B : Integer;
   begin
      Source_A_14.Read (Level_A);
      Source_B_14.Read (Level_B);
      Level := Level_A + Level_B;
   end Read_Power;
end Power_14;

Specifications of Private Children in SPARK 2014:

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

Bodies of Private Children in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
package body Power_14.Source_A_14
  with SPARK_Mode,
       Refined_State => (State => S)
is
   S : Integer := 0;

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

   procedure Read (Level : out Integer)
     with Refined_Global  => (Input => S),
          Refined_Depends => (Level => S)
   is
   begin
      Level := S;
   end Read;
end Power_14.Source_B_14;

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

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

Specification in SPARK 2005:

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

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
package body Power_05
--# own State is Source_A.State,
--#              Source_B.State;
is

  --  Embedded package spec for Source_A
  package Source_A
  --# own State;        
  is
     procedure Read (Level : out Integer);
      --# global State;
      --# derives Level from State;
  end Source_A;

  --  Embedded package spec for Source_B.
  package Source_B
  --# own State;
  is
    procedure Read (Level : out Integer);
    --# global State;
    --# derives Level from State;
  end Source_B;

  --  Embedded package body for Source_A
  package body Source_A
  is
    State : Integer;

    procedure Read (Level : out Integer)
    is
    begin
      Level := State;
    end Read;
  end Source_A;

  --  Embedded package body for Source_B
  package body Source_B
  is
    State : Integer;

    procedure Read (Level : out Integer)
    is
    begin
      Level := State;
    end Read;

  end Source_B;

  procedure Read_Power(Level : out Integer)
  --# global Source_A.State, Source_B.State;
  --# derives
  --#     Level
  --#     from
  --#         Source_A.State,
  --#         Source_B.State;
  is
     Level_A : Integer;
     Level_B : Integer;
  begin
     Source_A. Read (Level_A);
     Source_B.Read (Level_B);
     Level := Level_A + Level_B;
  end Read_Power;

end Power_05;

Specification in SPARK 2014:

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

Body in SPARK 2014:

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

      procedure Read (Level : out Integer)
        with Global  => State,
             Depends => (Level => State);
   end Source_A;

   --  Embedded package spec for Source_B.
   package Source_B
     with Initializes => State
   is
      State : Integer := 0;

      procedure Read (Level : out Integer)
        with Global  => State,
             Depends => (Level => State);
   end Source_B;

   --  Embedded package body for Source_A
   package body Source_A is
      procedure Read (Level : out Integer) is
      begin
         Level := State;
      end Read;
   end Source_A;

   --  Embedded package body for Source_B
   package body Source_B is
      procedure Read (Level : out Integer) is
      begin
         Level := State;
      end Read;
   end Source_B;

   procedure Read_Power(Level : out Integer)
     with Refined_Global  => (Source_A.State,
                              Source_B.State),
          Refined_Depends => (Level => (Source_A.State,
                                        Source_B.State))
   is
      Level_A : Integer;
      Level_B : Integer;
   begin
      Source_A. Read (Level_A);
      Source_B.Read (Level_B);
      Level := Level_A + Level_B;
   end Read_Power;
end Power_14;

Private, abstract state, refining onto mixture of the above

This example is based around the packages from sections Private, abstract state, refining onto state of private child and Private, abstract state, refining onto concrete state of embedded package. Source_A is an embedded package, while Source_B is a private child. In order to avoid repetition, the code of this example is not being presented.

External Variables

Basic Input and Output Device Drivers

The following example shows a main program - Copy - that reads all available data from a given input port, stores it internally during the reading process in a stack and then outputs all the data read to an output port. The specifications of the stack packages are not presented since they are identical to previous examples.

Specification of main program in SPARK 2005:

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

Specification of input port in SPARK 2005:

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

end Input_Port_05;

Body of input port in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
package body Input_Port_05
is

   Input_State : Integer;
   for Input_State'Address use
     System.Storage_Elements.To_Address (16#ACECAE0#);
   pragma Volatile (Input_State);

   procedure Read_From_Port(Input_Value : out Integer)
   is
   begin
      Input_Value := Input_State;
   end Read_From_Port;

end Input_Port_05;

Specification of output port in SPARK 2005:

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

Body of output port in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
package body Output_Port_05
is

   Output_State : Integer;
   for Output_State'Address use
     System.Storage_Elements.To_Address (16#ACECAF0#);
   pragma Volatile (Output_State);

   procedure Write_To_Port(Output_Value : in Integer)
   is
   begin
      Output_State := Output_Value;
   end Write_To_Port;

end Output_Port_05;

Specification of main program in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
with Input_Port_14,
     Output_Port_14,
     Stacks_14;
--  No need to specify that Copy_14 is a main program

procedure Copy_14
  with SPARK_Mode,
       Global  => (Input  => Input_Port_14.Input_State,
                   Output => Output_Port_14.Output_State),
       Depends => (Output_Port_14.Output_State => Input_Port_14.Input_State)
is
   The_Stack   : Stacks_14.Stack;
   Value       : Integer;
   Done        : Boolean;
   Final_Value : constant Integer := 999;
begin
   Stacks_14.Clear(The_Stack);
   loop
      Input_Port_14.Read_From_Port(Value);
      Stacks_14.Push(The_Stack, Value);
      Done := Value = Final_Value;
      exit when Done;
   end loop;
   loop
      Stacks_14.Pop(The_Stack, Value);
      Output_Port_14.Write_To_Port(Value);
      exit when Stacks_14.Is_Empty(The_Stack);
   end loop;
end Copy_14;

Specification of input port in SPARK 2014:

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

Specification of output port in SPARK 2014:

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

Body of input port in SPARK 2014:

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
with System.Storage_Elements;

package body Input_Port_14
  with SPARK_Mode,
       Refined_State => (Input_State => Input_S)
is
   Input_S : Integer
     with Volatile,
          Async_Writers,
          Address => System.Storage_Elements.To_Address (16#ACECAE0#);

   procedure Read_From_Port(Input_Value : out Integer)
     with Refined_Global  => (Input => Input_S),
          Refined_Depends => (Input_Value => Input_S)
   is
   begin
      Input_Value := Input_S;
   end Read_From_Port;
end Input_Port_14;

Body of output port in SPARK 2014:

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
with System.Storage_Elements;

package body Output_Port_14
  with SPARK_Mode,
       Refined_State => (Output_State => Output_S)
is
   Output_S : Integer
     with Volatile,
          Async_Readers,
          Address => System.Storage_Elements.To_Address (16#ACECAF0#);

   procedure Write_To_Port(Output_Value : in Integer)
     with Refined_Global  => (Output => Output_S),
          Refined_Depends => (Output_S => Output_Value)
   is
   begin
      Output_S := Output_Value;
   end Write_To_Port;
end Output_Port_14;

Input driver using ‘Tail in a contract

This example uses the Input_Port package from section Basic Input and Output Device Drivers and adds a contract using the ‘Tail attribute. The example also use the Always_Valid attribute in order to allow proof to succeed (otherwise, there is no guarantee in the proof context that the value read from the port is of the correct type).

SPARK 2014 does not have the attribute ‘Tail but, often, an equivalent proof can be achieved using assert pragmas. Neither is there a direct equivalent of the Always_Valid attribute but the paragma Assume may be used to the same effect.

Specification in SPARK 2005:

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

end Input_Port;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
package body Input_Port
is

   Inputs : Integer;
   for Inputs'Address use
     System.Storage_Elements.To_Address (16#ACECAF0#);

   --# assert Inputs'Always_Valid;
   pragma Volatile (Inputs);

   procedure Read_From_Port(Input_Value : out Integer)
   is
   begin
      Input_Value := Inputs;
      if Input_Value = 0 then
         Input_Value := Inputs;
      end if;
   end Read_From_Port;

end Input_Port;

Specification in SPARK 2014:

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

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
with System.Storage_Elements;

package body Input_Port_14
  with SPARK_Mode,
       Refined_State => (Inputs => Input_Port)
is
   Input_Port : Integer
     with Volatile,
          Async_Writers,
          Address => System.Storage_Elements.To_Address (16#ACECAF0#);

   procedure Read_From_Port(Input_Value : out Integer)
     with Refined_Global  => Input_Port,
          Refined_Depends => (Input_Value => Input_Port)
   is
      First_Read  : Integer;
      Second_Read : Integer;
   begin
      Second_Read := Input_Port;    -- Ensure Second_Read is initialized
      pragma Assume (Second_Read'Valid);
      First_Read  := Second_Read;   -- but it is infact the First_Read.
      if First_Read = 0 then
         Second_Read := Input_Port; -- Now it is the Second_Read
         pragma Assume (Second_Read'Valid);
         Input_Value := Second_Read;
      else
         Input_Value := First_Read;
      end if;
      pragma Assert ((First_Read = 0 and then Input_Value = Second_Read)
                     or else (Input_Value = First_Read));
   end Read_From_Port;
end Input_Port_14;

Output driver using ‘Append in a contract

This example uses the Output package from section Basic Input and Output Device Drivers and adds a contract using the ‘Append attribute.

SPARK 2014 does not have the attribute ‘Append but, often, an equivalent proof can be achieved using assert pragmas.

Specification in SPARK 2005:

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

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
package body Output_Port
is

   Outputs : Integer;
   for Outputs'Address use System.Storage_Elements.To_Address (16#ACECAF10#);
   pragma Volatile (Outputs);

   procedure Write_To_Port(Output_Value : in Integer)
   is
   begin
      if Output_Value = -1 then
         Outputs := 0;
      end if;

      Outputs := Output_Value;
   end Write_To_Port;

end Output_Port;

Specification in SPARK 2014:

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

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
with System.Storage_Elements;

package body Output_Port_14
  with SPARK_Mode,
       Refined_State => (Outputs => Output_Port)
is
   Output_Port : Integer
     with Volatile,
          Async_Readers,
          Address => System.Storage_Elements.To_Address (16#ACECAF10#);

   -- This is a simple subprogram that always updates the Output_Shadow with
   -- the single value which is written to the output port.
   procedure Write_It (Output_Value : in Integer; Output_Shadow : out Integer)
     with Global  => (Output => Output_Port),
          Depends => ((Output_Port, Output_Shadow) => Output_Value),
          Post    => Output_Shadow = Output_Value
   is
   begin
      Output_Shadow := Output_Value;
      Output_Port := Output_Shadow;
   end Write_It;


   procedure Write_To_Port(Output_Value : in Integer)
     with Refined_Global  => (Output => Output_Port),
          Refined_Depends => (Output_Port => Output_Value)
   is
      Out_1, Out_2 : Integer;
   begin
      if Output_Value = -1 then
         Write_It (0, Out_1);
         Write_It (Output_Value, Out_2);
      else
         Write_It (Output_Value, Out_1);
         Out_2 := Out_1;  -- Avoids flow error.
      end if;

      pragma Assert (if Output_Value = -1 then
                        Out_1 = 0 and Out_2 = Output_Value
                     else
                        Out_1 = Output_Value);
   end Write_To_Port;
end Output_Port_14;

Refinement of external state - voting input switch

The following example presents an abstract view of the reading of 3 individual switches and the voting performed on the values read.

Abstract Switch specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
package Switch
--# own in State;
is

   type Reading is (on, off, unknown);

   function ReadValue return Reading;
   --# global in State;

end Switch;

Component Switch specifications in SPARK 2005:

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

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

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

end Switch.Val3;

Switch body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
with Switch.Val1;
with Switch.Val2;
with Switch.Val3;
package body Switch
--# own State is in Switch.Val1.State,
--#              in Switch.Val2.State,
--#              in Switch.Val3.State;
is

   subtype Value is Integer range -1 .. 1;
   subtype Score is Integer range -3 .. 3;
   type ConvertToValueArray is array (Reading) of Value;
   type ConvertToReadingArray is array (Score) of Reading;

   ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(on => 1,
                                                                         unknown => 0,
                                                                         off => -1);
   ConvertToReading : constant ConvertToReadingArray :=
                                      ConvertToReadingArray'(-3 .. -2 => off,
                                                             -1 .. 1 => unknown,
                                                             2 ..3 => on);

   function ReadValue return Reading
   --# global in Val1.State;
   --#        in Val2.State;
   --#        in Val3.State;
   is
      A, B, C : Reading;
   begin
       A := Val1.Read;
       B := Val2.Read;
       C := Val3.Read;
       return ConvertToReading (ConvertToValue (A) +
          ConvertToValue (B) + ConvertToValue (C));
   end ReadValue;

end Switch;

Abstract Switch specification in SPARK 2014:

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

   function ReadValue return Reading
     with Volatile_Function,
          Global => (Input => State);
end Switch;

Component Switch specifications in SPARK 2014:

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

Switch body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
with Switch.Val1,
     Switch.Val2,
     Switch.Val3;

package body Switch
   -- State is refined onto three states, each of which has properties
   --  Volatile and Input
  with SPARK_Mode,
       Refined_State => (State => (Switch.Val1.State,
                                   Switch.Val2.State,
                                   Switch.Val3.State))
is
   subtype Value is Integer range -1 .. 1;
   subtype Score is Integer range -3 .. 3;
   type ConvertToValueArray is array (Reading) of Value;
   type ConvertToReadingArray is array (Score) of Reading;

   ConvertToValue : constant ConvertToValueArray :=
     ConvertToValueArray'(on => 1,
                          unknown => 0,
                          off => -1);
   ConvertToReading : constant ConvertToReadingArray :=
     ConvertToReadingArray'(-3 .. -2 => off,
                            -1 .. 1  => unknown,
                             2 .. 3  => on);

   function ReadValue return Reading
     with Refined_Global => (Input => (Val1.State, Val2.State, Val3.State))
   is
      A, B, C : Reading;
   begin
      A := Val1.Read;
      B := Val2.Read;
      C := Val3.Read;
      return ConvertToReading (ConvertToValue (A) +
        ConvertToValue (B) + ConvertToValue (C));
   end ReadValue;
end Switch;

Complex I/O Device

The following example illustrates a more complex I/O device: the device is fundamentally an output device but an acknowledgement has to be read from it. In addition, a local register stores the last value written to avoid writes that would just re-send the same value. The own variable is then refined into a normal variable, an input external variable and an output external variable.

Specification in SPARK 2005:

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

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
package body Device
--# own State is        OldX,
--#              in     StatusPort,
--#                 out Register;
-- refinement on to mix of external and ordinary variables
is
   type Status_Port_Type is mod 2**32;

  OldX : Integer := 0; -- only component that needs initialization
  StatusPort : Status_Port_Type;
  pragma Volatile (StatusPort);
  -- address clause would be added here
  
  Register : Integer;
  pragma Volatile (Register);
  -- address clause would be added here

  procedure WriteReg (X : in Integer)
  --# global out Register;
  --# derives Register from X;
  is
  begin
    Register := X;
  end WriteReg;

  procedure ReadAck (OK : out Boolean)
  --# global in StatusPort;
  --# derives OK from StatusPort;
  is
    RawValue : Status_Port_Type;
  begin
    RawValue := StatusPort; -- only assignment allowed here
    OK := RawValue = 16#FFFF_FFFF#;
  end ReadAck;

  procedure Write (X : in Integer)
  --# global in out OldX; 
  --#           out Register; 
  --#        in     StatusPort;
  --# derives OldX,Register from OldX, X &
  --#         null          from StatusPort; 
  is
    OK : Boolean;
  begin
    if X /= OldX then
      OldX := X;
      WriteReg (X);
      loop
        ReadAck (OK);
        exit when OK;
      end loop; 
    end if;
  end Write;
end Device;

Specification in SPARK 2014:

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

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
package body Device
  with SPARK_Mode,
       Refined_State => (State => (OldX,
                                   StatusPort,
                                   Register))
   -- refinement on to mix of external and ordinary variables
is
   type Status_Port_Type is mod 2**32;

   OldX : Integer := 0; -- only component that needs initialization

   StatusPort : Status_Port_Type
     with Volatile,
          Async_Writers;
   -- address clause would be added here

   Register : Integer
     with Volatile,
          Async_Readers;
   -- address clause would be added here

   procedure WriteReg (X : in Integer)
     with Global  => (Output => Register),
          Depends => (Register => X)
   is
   begin
      Register := X;
   end WriteReg;

   procedure ReadAck (OK : out Boolean)
     with Global  => (Input => StatusPort),
          Depends => (OK => StatusPort)
   is
      RawValue : Status_Port_Type;
   begin
      RawValue := StatusPort; -- only assignment allowed here
      OK := RawValue = 16#FFFF_FFFF#;
   end ReadAck;

   procedure Write (X : in Integer)
     with Refined_Global  => (Input  => StatusPort,
                              Output => Register,
                              In_Out => OldX),
          Refined_Depends => ((OldX,
                               Register) => (OldX,
                                             X),
                               null => StatusPort)
   is
      OK : Boolean;
   begin
      if X /= OldX then
         OldX := X;
         WriteReg (X);
         loop
            ReadAck (OK);
            exit when OK;
         end loop;
      end if;
   end Write;
end Device;

Increasing values in input stream

The following example illustrates an input port from which values are read. According to its postcondition, procedure Increases checks whether the first values read from the sequence are in ascending order. This example shows that postconditions can refer to multiple individual elements of the input stream.

In SPARK 2014 we can use assert pragmas in the subprogram instead of specifying the action in the postcondition, as was done in Input driver using ‘Tail in a contract. Another alternative, as shown in this example, is to use a formal parameter of a private type to keep a trace of the values read.

Specification in SPARK 2005:

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

end Inc;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
with System.Storage_Elements;
package body Inc
-- Cannot refine own variable Sensor as it has been given a concrete type.
is
   Sensor : Integer;
   for Sensor'Address use System.Storage_Elements.To_Address (16#DEADBEE0#);
   pragma Volatile (Sensor);

   procedure Read (V     : out Integer;
                   Valid : out Boolean)
   --# global in Sensor;
   --# post (Valid -> V = Sensor~) and
   --#      (Sensor = Sensor'Tail (Sensor~));
   is
      Tmp : Integer;
   begin
      Tmp := Sensor;
      if Tmp'Valid then
         V := Tmp;
         Valid := True;
         --# check Sensor = Sensor'Tail (Sensor~);
      else
         V := 0;
         Valid := False;
      end if;
   end Read;

   procedure Increases (Result : out Boolean;
                        Valid  : out Boolean)
   is
      A, B : Integer;
   begin
      Result := False;
      Read (A, Valid);
      if Valid then
         Read (B, Valid);
         if Valid then
            Result := B > A;
         end if;
      end if;
   end Increases;

end Inc;

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
package Inc
  with SPARK_Mode,
       Abstract_State => (Sensor with External => Async_Writers)
is
   -- Declare a private type which will keep a trace of the
   -- values read.
   type Increasing_Indicator is private;

   -- Access (ghost) functions for the private type only intended for
   -- use in pre and post conditions or other assertion expressions
   function First (Indicator : Increasing_Indicator) return Integer
     with Ghost;

   function Second (Indicator : Increasing_Indicator) return Integer
     with Ghost;

   -- Used to check that the value returned by procedure Increases
   -- is valid (Invalid values have not been read from the Sensor).
   function Is_Valid (Indicator : Increasing_Indicator) return Boolean;

   -- Use this function to determine whether the result of the procedure
   -- Increases indicates an increasing value.
   -- It can only be called if Is_Valid (Indicator)
   function Is_Increasing (Indicator : Increasing_Indicator) return Boolean
     with Pre => Is_Valid (Indicator);

   procedure Increases (Result : out Increasing_Indicator)
     with Global => Sensor,
          Post   => (if Is_Valid (Result) then Is_Increasing (Result)=
                       (Second (Result) > First (Result)));

private
   type Increasing_Indicator is record
      Valid : Boolean;
      First, Second : Integer;
   end record;
end Inc;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
with System.Storage_Elements;

package body Inc
  with SPARK_Mode,
       Refined_State => (Sensor => S)
is
   pragma Warnings (Off);
   S : Integer
     with Volatile,
          Async_Writers,
          Address => System.Storage_Elements.To_Address (16#DEADBEE0#);
   pragma Warnings (On);

   function First (Indicator : Increasing_Indicator) return Integer is
     (Indicator.First);

   function Second (Indicator : Increasing_Indicator) return Integer is
     (Indicator.Second);

   function Is_Valid (Indicator : Increasing_Indicator) return Boolean is
     (Indicator.Valid);

   function Is_Increasing (Indicator : Increasing_Indicator) return Boolean is
     (Indicator.Second > Indicator.First);

   pragma Warnings (Off);
   procedure Read (V     : out Integer;
                   Valid : out Boolean)
     with Global => S,
          Post   => (if Valid then V'Valid)
   is
      Tmp : Integer;
   begin
      pragma Warnings (On);
      Tmp := S;
      pragma Warnings (Off);
      if Tmp'Valid then
      pragma Warnings (On);
         V := Tmp;
         Valid := True;
      else
         V := 0;
         Valid := False;
      end if;
   end Read;

   procedure Increases (Result : out Increasing_Indicator)
     with Refined_Global => S
   is
   begin
      Read (Result.First, Result.Valid);
      if Result.Valid then
         Read (Result.Second, Result.Valid);
      else
         Result.Second := 0;
      end if;
   end Increases;
end Inc;

Package Inheritance

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

Contracts with remote state

The following example illustrates indirect access to the state of one package by another via an intermediary. Raw_Data stores some data, which has preprocessing performed on it by Processing and on which Calculate performs some further processing (although the corresponding bodies are not given, Read_Calculated_Value in Calculate calls through to Read_Processed_Data in Processing, which calls through to Read in Raw_Data).

Specifications in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
package Raw_Data
--# own State;
--# Initializes State;
is

   function Data_Is_Valid return Boolean;
   --# global State;

   function Get_Value return Integer;
   --# global State;

   procedure Read_Next;
   --# global in out State;
   --# derives State from State;


end Raw_Data;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Raw_Data;
--# inherit Raw_Data;
package Processing
--# own State;
--# Initializes State;
is

   procedure Get_Processed_Data (Value : out Integer);
   --# global in     Raw_Data.State;
   --#        in out State;
   --# derives Value, State  from State, Raw_Data.State;
   --# pre Raw_Data.Data_Is_Valid (Raw_Data.State);

end Processing;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
with Processing;
--# inherit Processing, Raw_Data;
package Calculate
is

   procedure Read_Calculated_Value (Value : out Integer);
   --# global in out Processing.State;
   --#        in     Raw_Data.State;
   --# derives Value, Processing.State from Processing.State, Raw_Data.State;
   --# pre Raw_Data.Data_Is_Valid (Raw_Data.State);

end Calculate;

Specifications in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
package Raw_Data
  with SPARK_Mode,
       Abstract_State => (State with External => Async_Writers),
       Initializes    => State
is
   function Data_Is_Valid return Boolean
     with Volatile_Function,
          Global => State;

   function Get_Value return Integer
     with Volatile_Function,
          Global => State;

   procedure Read_Next
     with Global  => (In_Out => State),
          Depends => (State => State);
end Raw_Data;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Raw_Data;

package Processing
  with SPARK_Mode,
       Abstract_State => State
is
   procedure Get_Processed_Data (Value : out Integer)
     with Global  => (Input  => Raw_Data.State,
                      In_Out => State),
          Depends => ((Value,
                       State) => (State,
                                  Raw_Data.State)),
          Pre     => Raw_Data.Data_Is_Valid;
end Processing;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Processing,
     Raw_Data;

package Calculate
  with SPARK_Mode
is
   procedure Read_Calculated_Value (Value : out Integer)
     with Global  => (In_Out => Processing.State,
                      Input  => Raw_Data.State),
          Depends => ((Value,
                       Processing.State) => (Processing.State,
                                             Raw_Data.State)),
          Pre     => Raw_Data.Data_Is_Valid;
end Calculate;

Package nested inside subprogram

This example is a modified version of that given in section Refinement of external state - voting input switch. It illustrates the use of a package nested within a subprogram.

Abstract Switch specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
package Switch
--# own in State;
is

   type Reading is (on, off, unknown);

   function ReadValue return Reading;
   --# global in State;

end Switch;

Component Switch specifications in SPARK 2005:

As in Refinement of external state - voting input switch

Switch body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
with Switch.Val1;
with Switch.Val2;
with Switch.Val3;
package body Switch
--# own State is in Switch.Val1.State,
--#              in Switch.Val2.State,
--#              in Switch.Val3.State;
is

   subtype Value is Integer range -1 .. 1;
   subtype Score is Integer range -3 .. 3;


   function ReadValue return Reading
   --# global in Val1.State;
   --#        in Val2.State;
   --#        in Val3.State;
   is
      A, B, C : Reading;

      --  Embedded package to provide the capability to synthesize three inputs
      --  into one.
      --# inherit Switch;
      package Conversion
      is

         function Convert_To_Reading
            (Val_A : Switch.Reading;
             Val_B : Switch.Reading;
             Val_C : Switch.Reading) return Switch.Reading;

      end Conversion;

      package body Conversion
      is

         type ConvertToValueArray is array (Switch.Reading) of Switch.Value;
         type ConvertToReadingArray is array (Switch.Score) of Switch.Reading;
         ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(Switch.on => 1,
                                                                         Switch.unknown => 0,
                                                                         Switch.off => -1);

         ConvertToReading : constant ConvertToReadingArray :=
                                      ConvertToReadingArray'(-3 .. -2 => Switch.off,
                                                             -1 .. 1  => Switch.unknown,
                                                             2 ..3    => Switch.on);

         function Convert_To_Reading
            (Val_A : Switch.Reading;
             Val_B : Switch.Reading;
             Val_C : Switch.Reading) return Switch.Reading
         is
         begin

            return ConvertToReading (ConvertToValue (Val_A) +
                   ConvertToValue (Val_B) + ConvertToValue (Val_C));
         end Convert_To_Reading;

      end Conversion;
   
   begin
       A := Val1.Read;
       B := Val2.Read;
       C := Val3.Read;
       return Conversion.Convert_To_Reading
                (Val_A => A,
                 Val_B => B,
                 Val_C => C);
   end ReadValue;

end Switch;

Abstract Switch specification in SPARK 2014:

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

   function ReadValue return Reading
     with Volatile_Function,
          Global => (Input => State);
end Switch;

Component Switch specification in SPARK 2014:

As in Refinement of external state - voting input switch

Switch body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
with Switch.Val1,
     Switch.Val2,
     Switch.Val3;

package body Switch
  --  State is refined onto three states, each of which has properties
  --  Volatile and Input.
  with SPARK_Mode,
       Refined_State => (State => (Switch.Val1.State,
                                   Switch.Val2.State,
                                   Switch.Val3.State))
is
   subtype Value is Integer range -1 .. 1;
   subtype Score is Integer range -3 .. 3;

   function ReadValue return Reading
     with Refined_Global => (Input => (Val1.State, Val2.State, Val3.State))
   is
      A, B, C : Reading;

      --  Embedded package to provide the capability to synthesize three inputs
      --  into one.
      package Conversion is
         function Convert_To_Reading
           (Val_A : Switch.Reading;
            Val_B : Switch.Reading;
            Val_C : Switch.Reading) return Switch.Reading;
      end Conversion;

      package body Conversion is
         type ConvertToValueArray is array (Switch.Reading) of Switch.Value;
         type ConvertToReadingArray is array (Switch.Score) of Switch.Reading;
         ConvertToValue : constant ConvertToValueArray :=
           ConvertToValueArray'(Switch.on => 1,
                                Switch.unknown => 0,
                                Switch.off => -1);

         ConvertToReading : constant ConvertToReadingArray :=
           ConvertToReadingArray'(-3 .. -2 => Switch.off,
                                  -1 .. 1  => Switch.unknown,
                                   2 .. 3  => Switch.on);

         function Convert_To_Reading
            (Val_A : Switch.Reading;
             Val_B : Switch.Reading;
             Val_C : Switch.Reading) return Switch.Reading is
           (ConvertToReading (ConvertToValue (Val_A) +
                              ConvertToValue (Val_B) +
                              ConvertToValue (Val_C)));
      end Conversion;
   begin  --  begin statement of ReadValue function
      A := Val1.Read;
      B := Val2.Read;
      C := Val3.Read;
      return Conversion.Convert_To_Reading
               (Val_A => A,
                Val_B => B,
                Val_C => C);
   end ReadValue;
end Switch;

Circular dependence and elaboration order

SPARK 2005 avoided issues of circular dependence and elaboration order dependencies through a combination of the inherit annotation and the restrictions that initialization expressions are constant, user defined subprograms cannot be called in the sequence of statements of a package body and a package can only initialize variables declared in its delarative part.

SPARK 2014 does not have the inherit annotation and only enforces the restriction that a package can only initialize an object declared in its declarative region. Hence, in SPARK 2014 two package bodies that depend on each other’s specification may be legal, as is calling a user defined suprogram.

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

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

Package Specifications in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
package P_14
  with SPARK_Mode,
       Abstract_State => P_State,
       Initializes    => (P_State, Global_Var),
       Elaborate_Body
is
   Global_Var : Integer;

   procedure Init (S : out Integer);
end P_14;
1
2
3
4
5
6
7
8
9
package Q_14
  with SPARK_Mode,
       Abstract_State => Q_State,
       Initializes    => Q_State
is
   type T is new Integer;

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

Package Bodies in SPARK 2014

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
with Q_14;

package body P_14
  with SPARK_Mode,
       Refined_State => (P_State => P_S)
is
   P_S : Q_14.T;  -- The use of type Q.T does not require
                  -- the body of Q to be elaborated.

   procedure Init (S : out Integer) is
   begin
      S := 5;
   end Init;
begin
   -- Cannot call Q_14.Init here beacuse
   -- this would require an Elaborate_All for Q_14
   -- and would be detected as a circularity
   Init (Global_Var);
   P_S := Q_14.T (Global_Var);
end P_14;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
with P_14;
pragma Elaborate_All (P_14); -- Required because the elaboration of the
                             -- body of Q_14 (indirectly) calls P_14.Init
package body Q_14
  with SPARK_Mode,
       Refined_State => (Q_State => Q_S)
is
   Q_S : T;

   procedure Init (S : out T) is
      V : Integer;
   begin
      P_14.Init (V);
      if V > 0 and then  V <= Integer'Last - 5 then
         S := T(V + 5);
      else
         S := 5;
      end if;
   end Init;
begin
   Init (Q_S);
end Q_14;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
with Q_14;
pragma Elaborate_All (Q_14); -- Required because Q_14.Init is called
                             -- in the elaboration of the body of R_14
use type Q_14.T;

package body R_14
  with SPARK_Mode,
       Refined_State => (State => R_S)
is
   R_S : Q_14.T;
   procedure Op ( X : in Positive)
     with Refined_Global => (In_Out => R_S)
   is
   begin
      if R_S <= Q_14.T'Last - Q_14.T (X) then
         R_S := R_S + Q_14.T (X);
      else
         R_S := 0;
      end if;
   end Op;
begin
   Q_14.Init (R_S);
   if P_14.Global_Var > 0
     and then R_S <= Q_14.T'Last - Q_14.T (P_14.Global_Var)
   then
      R_S := R_S + Q_14.T (P_14.Global_Var);
   else
      R_S := Q_14.T (P_14.Global_Var);
   end if;
end R_14;

Bodies and Proof

Assert, Assume, Check contracts

Assert (in loop) contract

The following example demonstrates how the SPARK 2005 assert annotation is used inside a loop as a loop invariant. It cuts the loop and on each iteration of the loop the list of existing hypotheses for the path is cleared. A verification condition is generated to prove that the assert expression is True, and the expression is the basis of the new hypotheses.

SPARK 2014 has a specific pragma for defining a loop invariant, pragma Loop_Invariant which is more sophisticated than the SPARK 2005 assert annotation and often requires less conditions in the invariant expression than in SPARK 2005. As in SPARK 2005 a default loop invariant will be used if one is not provided which, often, may be sufficient to prove absence of run-time exceptions. Like all SPARK 2014 assertion expressions the loop invariant is executable.

Note in the example below the SPARK 2014 version proves absence of run-time exceptions without an explicit loop invariant being provided.

Specification in SPARK 2005:

1
2
3
4
5
6
7
8
package Assert_Loop_05
is
   subtype Index is Integer range 1 .. 10;
   type A_Type is Array (Index) of Integer;

   function Value_present (A: A_Type; X : Integer) return Boolean;
   --# return for some M in Index => (A (M) = X);
end Assert_Loop_05;

Body in SPARK 2005:

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

Specification in SPARK 2014:

1
2
3
4
5
6
7
8
9
package Assert_Loop_14
  with SPARK_Mode
is
   subtype Index is Integer range 1 .. 10;
   type A_Type is Array (Index) of Integer;

   function Value_present (A : A_Type; X : Integer) return Boolean
     with Post => Value_present'Result = (for some M in Index => A (M) = X);
end Assert_Loop_14;

Body in SPARK 2014:

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

      return A (I) = X;
   end Value_Present;
end Assert_Loop_14;

Assert (no loop) contract

While not in a loop, the SPARK 2005 assert annotation maps to pragma Assert_And_Cut in SPARK 2014. Both the assert annotation and pragma assert clear the list of hypotheses on the path, generate a verification condition to prove the assertion expression and use the assertion expression as the basis of the new hypotheses.

Assume contract

The following example illustrates use of an Assume annotation. The assumed expression does not generate a verification condition and is not proved (although it is executed in SPARK 2014 if assertion expressions are not ignored at run-time).

In this example, the Assume annotation is effectively being used to implement the SPARK 2005 Always_Valid attribute.

Specification for Assume annotation in SPARK 2005:

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

end Input_Port;

Body for Assume annotation in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
with System.Storage_Elements;
package body Input_Port
is

   Inputs : Integer;
   for Inputs'Address use System.Storage_Elements.To_Address (16#CAFE0#);
   pragma Volatile (Inputs);

   procedure Read_From_Port(Input_Value : out Integer)
   is
   begin
      --# assume Inputs in Integer;
      Input_Value := Inputs;
   end Read_From_Port;

end Input_Port;

Specification for Assume annotation in SPARK 2014:

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

Body for Assume annotation in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
with System.Storage_Elements;

package body Input_Port
  with SPARK_Mode,
       Refined_State => (State_Inputs => Inputs)
is
   Inputs : Integer
     with Volatile,
          Async_Writers,
          Address => System.Storage_Elements.To_Address (16#CAFE0#);

   procedure Read_From_Port(Input_Value : out Integer)
     with Refined_Global  => (Input => Inputs),
          Refined_Depends => (Input_Value => Inputs)
   is
   begin
      Input_Value := Inputs;
      pragma Assume(Input_Value in Integer);
   end Read_From_Port;
end Input_Port;

Check contract

The SPARK 2005 check annotation is replaced by pragma assert in SPARK 2014. This annotation generates a verification condition to prove the checked expression and adds the expression as a new hypothesis to the list of existing hypotheses.

Specification for Check annotation in SPARK 2005:

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

Body for Check annotation in SPARK 2005:

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

Specification for Check annotation in SPARK 2014:

1
2
3
4
5
6
7
8
package Check_14
  with SPARK_Mode
is
   subtype Small is Integer range 1 .. 10;
   subtype Big   is Integer range 1 .. 21;

   procedure Compare (A, B : in Small; C : in out Big);
end Check_14;

Body for Check annotation in SPARK 2014:

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

Assert used to control path explosion

This capability is in general not needed with the SPARK 2014 toolset where path explosion is handled automatically. In the rare cases where this is needed you can use pragma Assert_And_Cut.

Other Contracts and Annotations

Always_Valid assertion

See section Input driver using ‘Tail in a contract for use of an assertion involving the Always_Valid attribute.

Rule declaration annotation

See section Proof types and proof functions.

Proof types and proof functions

The following example gives pre- and postconditions on operations that act upon the concrete representation of an abstract own variable. This means that proof functions and proof types are needed to state those pre- and postconditions. In addition, it gives an example of the use of a rule declaration annotation - in the body of procedure Initialize - to introduce a rule related to the components of a constant record value.

SPARK 2014 does not have a direct equivalent of proof types and proof functions. State abstractions cannot have a type and all functions in SPARK 2014 are Ada functions. Functions may be defined to be ghost functions which means that they can only be called within an assertion expression such as a pre or postcondition. Assertion expressions may be executed or ignored at run-time and if they are ignored Ghost functions behave much like SPARK 2005 proof functions.

Rule declaration annotations for structured constants are not required in SPARK 2014.

The SPARK 2005 version of the example given below will require user defined proof rules to discharge the proofs because refined definitions of some of the proof functions cannot be provided as they would have different formal parameters. The SPARK 2014 version does not suffer from this problem as functions called within assertion expressions may have global items.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
package Stack
--# own State : Abstract_Stack;
is
   --  It is not possible to specify that the stack will be
   --  initialized to empty except by having an initialization
   --  subprogram called during program execution (as opposed to
   --  package elaboration).

   --  Proof functions to indicate whether or not the Stack is empty
   --  and whether or not it is full.
   --# type Abstract_Stack is abstract;

   --# function Max_Stack_Size return Natural;

   --  Proof function to give the number of elements on the stack.
   --# function Count(Input : Abstract_Stack) return Natural;

   --  Proof function returns the Nth entry on the stack.
   --  Stack_Entry (Count (State)) is the top of stack
   --# function Stack_Entry (N : Natural; S : Abstract_Stack) return Integer;
   --# pre N in 1 .. Count (S);
   --  A refined version of this function cannot be written because
   --  the abstract view has a formal parameter of type Abstract_Stack
   --  whereas the refined view would not have this parameter but use
   --  a global. A user defined proof rule would be required to define
   --  this function. Alternatively, it could be written as an Ada
   --  function where the the global and formal parameter views would
   --  be available. However, the function would then be callable and
   --  generate implementation code.

   --# function Is_Empty(Input : Abstract_Stack) return Boolean;
   --# return Count (Input) = 0;

   --# function Is_Full(Input : Abstract_Stack) return Boolean;
   --# return Count (Input) = Max_Stack_Size;

   --  The precondition requires the stack is not full when a value, X,
   --  is pushed onto it.
   --  The postcondition indicates that the count of the stack will be
   --  incremented after a push and therefore the stack will be non-empty.
   --  The item X is now the top of the stack.
   procedure Push(X : in Integer);
   --# global in out State;
   --# pre  not Is_Full(State);
   --# post Count (State) = Count (State~) + 1 and
   --#      Count (State) <= Max_Stack_Size and
   --#      Stack_Entry (Count (State), State) = X;

   --  The precondition requires the stack is not empty when we
   --  pull a value from it.
   --  The postcondition indicates the stack count is decremented.
   procedure Pop (X : out Integer);
   --# global in out State;
   --# pre not Is_Empty (State);
   --# post Count (State) = Count (State~) - 1;

   --  Procedure that swaps the first two elements in a stack.
   procedure Swap2;
   --# global in out State;
   --# pre  Count(State) >= 2;
   --# post Count(State) =  Count(State~) and
   --#      Stack_Entry (Count (State), State) =
   --#         Stack_Entry (Count (State) - 1, State~) and
   --#      Stack_Entry (Count (State) - 1, State) =
   --#         Stack_Entry (Count (State), State~);

   --  Initializes the Stack.
   procedure Initialize;
   --# global out State;
   --# post Is_Empty (State);
end Stack;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
package body Stack
--# own State is My_Stack;
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   type Stack_Type is record
      S : Vector;
      Pointer : Pointer_Range;
   end record;

   Initial_Stack : constant Stack_Type :=
      Stack_Type'(S       => Vector'(others => 0),
                  Pointer => 0);

   My_Stack : Stack_Type;

   procedure Push(X : in Integer)
   --# global in out My_Stack;
   --# pre My_Stack.Pointer < Stack_Size;
   is
   begin
      My_Stack.Pointer := My_Stack.Pointer + 1;
      My_Stack.S(My_Stack.Pointer) := X;
   end Push;

   procedure Pop (X : out Integer)
   --# global in out My_Stack;
   --# pre My_Stack.Pointer >= 1;
   is
   begin
      X := My_Stack.S (My_Stack.Pointer);
      My_Stack.Pointer := My_Stack.Pointer - 1;
   end Pop;

   procedure Swap2
   --# global in out My_Stack;
   --# post My_Stack.Pointer = My_Stack~.Pointer;
   is
      Temp : Integer;
   begin
      Temp := My_Stack.S (1);
      My_Stack.S (1) := My_Stack.S (2);
      My_Stack.S (2) := Temp;
   end Swap2;

   procedure Initialize
   --# global out My_Stack;
   --# post My_Stack.Pointer = 0;
   is
      --# for Initial_Stack declare Rule;
   begin
      My_Stack := Initial_Stack;
   end Initialize;
end Stack;

Specification in SPARK 2014

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
package Stack
  with SPARK_Mode,
       Abstract_State    => State,
       Initializes       => State,
       Initial_Condition => Is_Empty
is
   --  In SPARK 2014 we can specify an initial condition for the
   --  elaboration of a package and so initialization may be done
   --  during the elaboration of the package Stack, rendering the need
   --  for an initialization procedure unnecessary.

   --  Abstract states do not have types in SPARK 2014 they can only
   --  be directly referenced in Global and Depends aspects.

   --  Proof functions are actual functions but they may have the
   --  convention Ghost meaning that they can only be called from
   --  assertion expressions, e.g., pre and postconditions
   function Max_Stack_Size return Natural
     with Ghost;

   -- Returns the number of elements on the stack
   function Count return Natural
     with Global     => (Input => State),
          Ghost;

   --  Returns the Nth entry on the stack. Stack_Entry (Count) is the
   --  top of stack
   function Stack_Entry (N : Natural) return Integer
     with Global     => (Input => State),
          Pre        => N in 1 .. Count,
          Ghost;
   --  A body (refined) version of this function can (must) be
   --  provided in the body of the package.

   function Is_Empty return Boolean is (Count = 0)
     with Global     => State,
          Ghost;

   function Is_Full return Boolean is (Count = Max_Stack_Size)
     with Global     => State,
          Ghost;

   --  The precondition requires the stack is not full when a value,
   --  X, is pushed onto it. Functions with global items (Is_Full
   --  with global State in this case) can be called in an assertion
   --  expression such as the precondition here.  The postcondition
   --  indicates that the count of the stack will be incremented after
   --  a push and therefore the stack will be non-empty.  The item X
   --  is now the top of the stack.
   procedure Push (X : in Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Full,
          Post   => Count = Count'Old + 1 and
                    Count <= Max_Stack_Size and
                    Stack_Entry (Count) = X;

   --  The precondition requires the stack is not empty when we pull a
   --  value from it. The postcondition indicates the stack count is
   --  decremented.
   procedure Pop (X : out Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Empty,
          Post   => Count = Count'Old - 1;

   --  Procedure that swaps the top two elements in a stack.
   procedure Swap2
     with Global => (In_Out => State),
          Pre    => Count >= 2,
          Post   => Count = Count'Old and
                    Stack_Entry (Count) = Stack_Entry (Count - 1)'Old and
                    Stack_Entry (Count - 1) = Stack_Entry (Count)'Old;
end Stack;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
package body Stack
  with SPARK_Mode,
       Refined_State => (State => My_Stack)
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1 .. Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   type Stack_Type is record
      S : Vector;
      Pointer : Pointer_Range;
   end record;

   Initial_Stack : constant Stack_Type :=
     Stack_Type'(S       => Vector'(others => 0),
                 Pointer => 0);
   My_Stack : Stack_Type;

   function Max_Stack_Size return Natural is (Stack_Size);

   function Count return Natural is (Natural (My_Stack.Pointer))
     with Refined_Global => My_Stack;

   function Stack_Entry (N : Natural) return Integer is
     (My_Stack.S (Index_Range (N)))
     with Refined_Global => My_Stack;


   procedure Push(X : in Integer)
     with Refined_Global => (In_Out => My_Stack)
   is
   begin
      My_Stack.Pointer := My_Stack.Pointer + 1;
      My_Stack.S(My_Stack.Pointer) := X;
   end Push;

   procedure Pop (X : out Integer)
     with Refined_Global => (In_Out => My_Stack)
   is
   begin
      X := My_Stack.S (My_Stack.Pointer);
      My_Stack.Pointer := My_Stack.Pointer - 1;
   end Pop;

   procedure Swap2
     with Refined_Global => (In_Out => My_Stack)
   is
      Temp : Integer;
   begin
      Temp := My_Stack.S (My_Stack.Pointer);
      My_Stack.S (My_Stack.Pointer) := My_Stack.S (My_Stack.Pointer - 1);
      My_Stack.S (My_Stack.Pointer - 1) := Temp;
   end Swap2;
begin
   My_Stack := Initial_Stack;
end Stack;

Using an External Prover

One may wish to use an external prover such as Isabelle, with rules defining a ghost function written in the prover input language. This can be done in SPARK 2014 by denoting the ghost function as an Import in lieu of providing a body for it. Of course such ghost functions cannot be executed.

Specification in SPARK 2014 using an external prover:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
package Stack_External_Prover
  with SPARK_Mode,
       Abstract_State    => State,
       Initializes       => State,
       Initial_Condition => Is_Empty
is
   --  A Ghost function may be an Import which means that no body is
   --  given in the SPARK 2014 code and the proof has to be discharged
   --  by an external prover. Of course, such functions are not
   --  executable.
   function Max_Stack_Size return Natural
     with Global     => null,
          Ghost,
          Import;

   --  Returns the number of elements on the stack
   function Count return Natural
     with Global     => (Input => State),
          Ghost,
          Import;

   --  Returns the Nth entry on the stack. Stack_Entry (Count) is the
   --  top of stack
   function Stack_Entry (N : Natural) return Integer
     with Global     => (Input => State),
          Ghost,
          Import;

   function Is_Empty return Boolean
     with Global     => State,
          Ghost,
          Import;

   function Is_Full return Boolean
     with Global     => State,
          Ghost,
          Import;

   procedure Push (X : in Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Full,
          Post   => Count = Count'Old + 1 and Count <= Max_Stack_Size and
                    Stack_Entry (Count) = X;

   procedure Pop (X : out Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Empty,
          Post   => Count = Count'Old - 1;

   procedure Swap2
     with Global => (In_Out => State),
          Pre    => Count >= 2,
          Post   => Count = Count'Old and
                    Stack_Entry (Count) = Stack_Entry (Count - 1)'Old and
                    Stack_Entry (Count - 1) = Stack_Entry (Count)'Old;
end Stack_External_Prover;

Quoting an Own Variable in a Contract

Sometimes it is necessary to reference an own variable (a state abstraction) in a contract. In SPARK 2005 this was achieved by declaring the own variable with a type, either concrete or abstract. As seen in Proof types and proof functions. Once the own variable has a type it can be used in a SPARK 2005 proof context.

A state abstraction in SPARK 2014 does not have a type. Instead, an Ada type to represent the abstract state is declared. A function which has the state abstraction as a global item is then declared which returns an object of the type. This function may have the same name as the state abstraction (the name is overloaded). References which appear to be the abstract state in an assertion expression are in fact calls to the overloaded function.

An example of this technique is given in the following example which is a version of the stack example given in Proof types and proof functions but with the post conditions extended to express the functional properties of the stack.

The extension requires the quoting of the own variable/state abstraction in the postcondition in order to state that the contents of the stack other than the top entries are not changed.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
package Stack_Functional_Spec
--# own State : Abstract_Stack;
is
   --  It is not possible to specify that the stack will be
   --  initialized to empty except by having an initialization
   --  subprogram called during program execution (as opposed to
   --  package elaboration).

   --  Proof functions to indicate whether or not the Stack is empty
   --  and whether or not it is full.
   --# type Abstract_Stack is abstract;

   --# function Max_Stack_Size return Natural;

   --  Proof function to give the number of elements on the stack.
   --# function Count(Input : Abstract_Stack) return Natural;

   --  Proof function returns the Nth entry on the stack.
   --  Stack_Entry (Count (State)) is the top of stack
   --# function Stack_Entry (S : Abstract_Stack; N : Natural) return Integer;
   --# pre N in 1 .. Count (S);
   --  A refined version of this function cannot be written because
   --  the abstract view has a formal parameter of type Abstract_Stack
   --  whereas the refined view would not have this parameter but use
   --  a global. A user defined proof rule would be required to
   --  define this function. Alternatively, it could be written as an
   --  Ada function where the the global and formal parameter views
   --  would be available. However, the function would then be
   --  callable and generate implementation code.

   --# function Is_Empty(Input : Abstract_Stack) return Boolean;
   --# return Count (Input) = 0;

   --# function Is_Full(Input : Abstract_Stack) return Boolean;
   --# return Count (Input) = Max_Stack_Size;

   --  The precondition requires the stack is not full when a value, X,
   --  is pushed onto it.
   --  Functions with global items (Is_Full with global State in this case)
   --  can be called in an assertion expression such as the precondition here.
   --  The postcondition indicates that the count of the stack will be
   --  incremented after a push and therefore the stack will be non-empty.
   --  The item X is now the top of the stack and the contents of the rest of
   --  the stack are unchanged.
   procedure Push(X : in Integer);
   --# global in out State;
   --# pre  not Is_Full(State);
   --# post Count (State) = Count (State~) + 1 and
   --#      Count (State) <= Max_Stack_Size and
   --#      Stack_Entry (State, Count (State)) = X and
   --#      (for all I in Natural range 1 .. Count (State~) =>
   --#          (Stack_Entry (State, I) = Stack_Entry (State~, I)));

   --  The precondition requires the stack is not empty when we
   --  pull a value from it.
   --  The postcondition indicates that the X = the old top of stack,
   --  the stack count is decremented, and the contents of the stack excluding
   --  the old top of stack are unchanged.
   procedure Pop (X : out Integer);
   --# global in out State;
   --# pre not Is_Empty (State);
   --# post Count (State) = Count (State~) - 1 and
   --#      X = Stack_Entry (State~, Count (State~)) and
   --#      (for all I in Natural range 1 .. Count (State) =>
   --#          (Stack_Entry (State, I) = Stack_Entry (State~, I)));

   --  The precondition requires that the stack has at least 2 entries
   --  (Count >= 2).
   --  The postcondition states that the top two elements of the stack are
   --  transposed but the remainder of the stack is unchanged.
   procedure Swap2;
   --# global in out State;
   --# pre  Count(State) >= 2;
   --# post Count(State) =  Count(State~) and
   --#      Stack_Entry (State, Count (State)) =
   --#         Stack_Entry (State~, Count (State) - 1) and
   --#      Stack_Entry (State, Count (State) - 1) =
   --#         Stack_Entry (State~, Count (State)) and
   --#      (for all I in Natural range 1 .. Count (State) =>
   --#          (Stack_Entry (State, I) = Stack_Entry (State~, I)));

   --  Initializes the Stack.
   procedure Initialize;
   --# global out State;
   --# post Is_Empty (State);
end Stack_Functional_Spec;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
package body Stack_Functional_Spec
--# own State is My_Stack;
is
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1..Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   type Stack_Type is
      record
         S : Vector;
         Pointer : Pointer_Range;
      end record;

   Initial_Stack : constant Stack_Type :=
      Stack_Type'(S       => Vector'(others => 0),
                  Pointer => 0);

   My_Stack : Stack_Type;

   procedure Push(X : in Integer)
   --# global in out My_Stack;
   --# pre My_Stack.Pointer < Stack_Size;
   is
   begin
      My_Stack.Pointer := My_Stack.Pointer + 1;
      My_Stack.S(My_Stack.Pointer) := X;
   end Push;

   procedure Pop (X : out Integer)
   --# global in out My_Stack;
   --# pre My_Stack.Pointer >= 1;
   is
   begin
      X := My_Stack.S (My_Stack.Pointer);
      My_Stack.Pointer := My_Stack.Pointer - 1;
   end Pop;

   procedure Swap2
   --# global in out My_Stack;
   --# post My_Stack.Pointer = My_Stack~.Pointer;
   is
      Temp : Integer;
   begin
      Temp := My_Stack.S (1);
      My_Stack.S (1) := My_Stack.S (2);
      My_Stack.S (2) := Temp;
   end Swap2;

   procedure Initialize
   --# global out My_Stack;
   --# post My_Stack.Pointer = 0;
   is
      --# for Initial_Stack declare Rule;
   begin
      My_Stack := Initial_Stack;
   end Initialize;

end Stack_Functional_Spec;

Specification in SPARK 2014

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
pragma Unevaluated_Use_Of_Old(Allow);
package Stack_Functional_Spec
  with SPARK_Mode,
       Abstract_State    => State,
       Initializes       => State,
       Initial_Condition => Is_Empty
is
   --  Abstract states do not have types in SPARK 2014 but to provide
   --  functional specifications it is sometimes necessary to refer to
   --  the abstract state in an assertion expression such as a post
   --  condition. To do this in SPARK 2014 an Ada type declaration is
   --  required to represent the type of the abstract state, then a
   --  function applied to the abstract state (as a global) can be
   --  written which returns an object of the declared type.
   type Stack_Type is private;

   --  The Abstract_State name may be overloaded by the function which
   --  represents it in assertion expressions.
   function State return Stack_Type
     with Global => State;

   function Max_Stack_Size return Natural
     with Ghost;

   --  Returns the number of elements on the stack
   --  A function may have a formal parameter (or return a value)
   --  of the abstract state.
   function Count (S : Stack_Type) return Natural
     with Ghost;

   -- Returns the Nth entry on the stack.
   -- Stack_Entry (S, Count (S)) is the top of stack
   function Stack_Entry (S : Stack_Type; N : Natural) return Integer
     with Pre        => N in 1 .. Count (S),
          Ghost;

   -- The ghost function Count can be called in the function
   -- expression because Is_Empty is also a ghost function.
   function Is_Empty return Boolean is (Count (State) = 0)
     with Global     => State,
          Ghost;

   function Is_Full return Boolean is (Count(State) = Max_Stack_Size)
     with Global     => State,
          Ghost;

   --  The precondition requires the stack is not full when a value, X,
   --  is pushed onto it.
   --  Functions with global items (Is_Full with global State in this case)
   --  can be called in an assertion expression such as the precondition here.
   --  The postcondition indicates that the count of the stack will be
   --  incremented after a push and therefore the stack will be non-empty.
   --  The item X is now the top of the stack and the contents of the rest of
   --  the stack are unchanged.
   procedure Push (X : in Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Full,
          Post   => Count (State) = Count (State'Old) + 1 and
                    Count (State) <= Max_Stack_Size and
                    Stack_Entry (State, Count (State)) = X and
                    (for all I in 1 .. Count (State'Old) =>
                        Stack_Entry (State, I) = Stack_Entry (State'Old, I));

   --  The precondition requires the stack is not empty when we
   --  pull a value from it.
   --  The postcondition indicates that the X = the old top of stack,
   --  the stack count is decremented, and the contents of the stack excluding
   --  the old top of stack are unchanged.
   procedure Pop (X : out Integer)
     with Global => (In_Out => State),
          Pre    => not Is_Empty,
          Post   => Count (State) = Count (State'Old) - 1 and
                    X = Stack_Entry (State'Old, Count (State'Old)) and
                   (for all I in 1 .. Count (State) =>
                       Stack_Entry (State, I) = Stack_Entry (State'Old, I));

   --  The precondition requires that the stack has at least 2 entries
   --  (Count >= 2).
   --  The postcondition states that the top two elements of the stack are
   --  transposed but the remainder of the stack is unchanged.
   procedure Swap2
     with Global => (In_Out => State),
          Pre    => Count (State) >= 2,
          Post   => Count(State) = Count (State'Old) and
                    Stack_Entry (State, Count (State)) =
                       Stack_Entry (State'Old, Count (State) - 1) and
                    Stack_Entry (State, Count (State) - 1) =
                       Stack_Entry (State'Old, Count (State)) and
                    (for all I in 1 .. Count (State) - 2 =>
                        Stack_Entry (State, I) = Stack_Entry (State'Old, I));

private
   -- The full type declarion used to represent the abstract state.
   Stack_Size : constant := 100;
   type    Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range   is Pointer_Range range 1 .. Stack_Size;
   type    Vector        is array(Index_Range) of Integer;

   type Stack_Type is record
      S : Vector;
      Pointer : Pointer_Range;
   end record;
end Stack_Functional_Spec;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
package body Stack_Functional_Spec
  with SPARK_Mode,
       Refined_State => (State => My_Stack)
is
   Initial_Stack : constant Stack_Type :=
     Stack_Type'(S       => Vector'(others => 0),
                 Pointer => 0);

   --  In this example the type used to represent the state
   --  abstraction and the actual type used in the implementation are
   --  the same, but they need not be. For instance S and Pointer
   --  could have been declared as distinct objects rather than
   --  composed into a record. Where the type representing the
   --  abstract state and the implementation of that state are
   --  different the function representing the abstract state has to
   --  convert implementation representation into the abstract
   --  representation. For instance, if S and Pointer were distinct
   --  objects the function State would have to return (S => S,
   --  Pointer => Pointer).
   My_Stack : Stack_Type;

   --  No convertion necessary as the abstract and implementation type
   --  is the same.
   function State return Stack_Type is (My_Stack)
     with Refined_Global => My_Stack;

   function Max_Stack_Size return Natural is (Stack_Size);

   function Count (S : Stack_Type) return Natural is (Natural (S.Pointer));

   function Stack_Entry (S : Stack_Type; N : Natural) return Integer is
     (S.S (Index_Range (N)));

   procedure Push(X : in Integer)
     with Refined_Global => (In_Out => My_Stack)
   is
   begin
      My_Stack.Pointer := My_Stack.Pointer + 1;
      My_Stack.S(My_Stack.Pointer) := X;
   end Push;

   procedure Pop (X : out Integer)
     with Refined_Global => (In_Out => My_Stack)
   is
   begin
      X := My_Stack.S (My_Stack.Pointer);
      My_Stack.Pointer := My_Stack.Pointer - 1;
   end Pop;

   procedure Swap2
     with Refined_Global => (In_Out => My_Stack)
   is
      Temp : Integer;
   begin
      Temp := My_Stack.S (My_Stack.Pointer);
      My_Stack.S (My_Stack.Pointer) := My_Stack.S (My_Stack.Pointer - 1);
      My_Stack.S (My_Stack.Pointer - 1) := Temp;
   end Swap2;
begin
   My_Stack := Initial_Stack;
end Stack_Functional_Spec;

Main_Program annotation

This annotation isn’t needed. Currently any parameterless procedure declared at library-level is considered as a potential main program and analyzed as such.

Update Expressions

SPARK 2005 has update expressions for updating records and arrays. They can only be used in SPARK 2005 proof contexts.

The equivalent in SPARK 2014 is the ‘Update attribute. This can be used in any Ada expression.

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
package Update_Examples
is
   type Rec is record
      X, Y : Integer;
   end record;

   type Index is range 1 ..3;

   type Arr is array (Index) of Integer;

   type Arr_2D is array (Index, Index) of Integer;

   type Nested_Rec is record
      A : Integer;
      B : Rec;
      C : Arr;
      D : Arr_2D;
   end record;

   type Nested_Arr is array (Index) of Nested_Rec;

   -- Simple record update
   procedure P1 (R : in out Rec);
   --# post R = R~ [X => 1];

   -- Simple 1D array update
   procedure P2 (A : in out Arr);
   --# post A = A~ [1 => 2];

   -- 2D array update
   procedure P3 (A2D : in out Arr_2D);
   --# post A2D = A2D~ [1, 1 => 1;
   --#                  2, 2 => 2;
   --#                  3, 3 => 3];

   -- Nested record update
   procedure P4 (NR : in out Nested_Rec);
   --# post NR = NR~ [A => 1;
   --#                B => NR~.B [X => 1];
   --#                C => NR~.C [1 => 5]];

   -- Nested array update
   procedure P5 (NA : in out Nested_Arr);
   --# post NA = NA~ [1 => NA~ (1) [A => 1;
   --#                              D => NA~ (1).D [2, 2 => 0]];
   --#                2 => NA~ (2) [B => NA~ (2).B [X => 2]];
   --#                3 => NA~ (3) [C => NA~ (3).C [1 => 5]]];
end Update_Examples;

Specification in SPARK 2014

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
package Update_Examples
  with SPARK_Mode
is
   type Rec is record
      X, Y : Integer;
   end record;

   type Arr is array (1 .. 3) of Integer;

   type Arr_2D is array (1 .. 3, 1 .. 3) of Integer;

   type Nested_Rec is record
      A : Integer;
      B : Rec;
      C : Arr;
      D : Arr_2D;
   end record;

   type Nested_Arr is array (1 .. 3) of Nested_Rec;

   -- Simple record update
   procedure P1 (R : in out Rec)
     with Post => R = R'Old'Update (X => 1);
   -- this is equivalent to:
   --   R = (X => 1,
   --        Y => R'Old.Y)

   -- Simple 1D array update
   procedure P2 (A : in out Arr)
     with Post => A = A'Old'Update (1 => 2);
   -- this is equivalent to:
   --   A = (1 => 2,
   --        2 => A'Old (2),
   --        3 => A'Old (3));

   -- 2D array update
   procedure P3 (A2D : in out Arr_2D)
     with Post => A2D = A2D'Old'Update ((1, 1) => 1,
                                        (2, 2) => 2,
                                        (3, 3) => 3);
   -- this is equivalent to:
   --   A2D = (1 => (1 => 1,
   --                2 => A2D'Old (1, 2),
   --                3 => A2D'Old (1, 3)),
   --          2 => (2 => 2,
   --                1 => A2D'Old (2, 1),
   --                3 => A2D'Old (2, 3)),
   --          3 => (3 => 3,
   --                1 => A2D'Old (3, 1),
   --                2 => A2D'Old (3, 2)));

   -- Nested record update
   procedure P4 (NR : in out Nested_Rec)
     with Post => NR = NR'Old'Update (A => 1,
                                      B => NR'Old.B'Update (X => 1),
                                      C => NR'Old.C'Update (1 => 5));
   -- this is equivalent to:
   --   NR = (A => 1,
   --         B.X => 1,
   --         B.Y => NR'Old.B.Y,
   --         C (1) => 5,
   --         C (2) => NR'Old.C (2),
   --         C (3) => NR'Old.C (3),
   --         D => NR'Old.D)

   -- Nested array update
   procedure P5 (NA : in out Nested_Arr)
     with Post =>
       NA = NA'Old'Update (1 => NA'Old (1)'Update
                                  (A => 1,
                                   D => NA'Old (1).D'Update ((2, 2) => 0)),
                           2 => NA'Old (2)'Update
                                  (B => NA'Old (2).B'Update (X => 2)),
                           3 => NA'Old (3)'Update
                                  (C => NA'Old (3).C'Update (1 => 5)));
   -- this is equivalent to:
   --   NA = (1 => (A => 1,
   --               B => NA'Old (1).B,
   --               C => NA'Old (1).C,
   --               D => NA'Old (1).D),
   --         2 => (B.X => 2,
   --               B.Y => NA'Old (2).B.Y,
   --               A => NA'Old (2).A,
   --               C => NA'Old (2).C,
   --               D => NA'Old (2).D),
   --         3 => (C => (1 => 5,
   --                     2 => NA'Old (3).C (2),
   --                     3 => NA'Old (3).C (3)),
   --               A => NA'Old (3).A,
   --               B => NA'Old (3).B,
   --               D => NA'Old (3).D));

end Update_Examples;

Value of Variable on Entry to a Loop

In SPARK 2005 the entry value of a for loop variable variable, X, can be referenced using the notation X%. This notation is required frequently when the variable is referenced in a proof context within the loop. Often it is needed to state that the value of X is not changed within the loop by stating X = X%. This notation is restricted to a variable which defines the lower or upper range of a for loop.

SPARK 2014 has a more general scheme whereby the loop entry value of any variable can be denoted within any sort of loop using the ‘Loop_Entry attribute. However, its main use is not for showing that the value of a for loop variable has not changed as the SPARK 2014 tools are able to determine this automatically. Rather it is used instead of ~ in loops because the attribute ‘Old is only permitted in postconditions (including Contract_Cases).

Specification in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
package Loop_Entry
is

  subtype ElementType is Natural range 0..1000;
  subtype IndexType is Positive range 1..100;
  type ArrayType is array (IndexType) of ElementType;

  procedure Clear (A: in out ArrayType; L,U: in IndexType);
  --# derives A from A, L, U;
  --# post (for all N in IndexType range L..U => (A(N) = 0)) and
  --#      (for all N in IndexType => ((N<L or N>U) -> A(N) = A~(N)));

end Loop_Entry;

Body in SPARK 2005:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
package body Loop_Entry
is

  procedure Clear (A: in out ArrayType; L,U: in IndexType)
  is
  begin
    for I in IndexType range L..U loop
      A(I) := 0;
      --# assert (for all N in IndexType range L..I => (A(N) = 0)) and
      --#        (for all N in IndexType => ((N<L or N>I) -> A(N) = A~(N))) and
      --#        U = U% and L <= I;
      -- Note U = U% is required to show that the vaule of U does not change
      -- within the loop.
    end loop;
  end Clear;

end Loop_Entry;

Specification in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
pragma SPARK_Mode (On);
package Loop_Entry
is

  subtype ElementType is Natural range 0..1000;
  subtype IndexType is Positive range 1..100;
  type ArrayType is array (IndexType) of ElementType;

   procedure Clear (A: in out ArrayType; L,U: in IndexType)
     with Depends => (A => (A, L, U)),
          Post    => (for all N in L..U => A(N) = 0) and
                     (for all N in IndexType =>
                         (if N<L or N>U then A(N) = A'Old(N)));

end Loop_Entry;

Body in SPARK 2014:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
pragma SPARK_Mode (On);
package body Loop_Entry
is

  procedure Clear (A: in out ArrayType; L,U: in IndexType)
  is
  begin
    for I in IndexType range L..U loop
      A(I) := 0;
         pragma Loop_Invariant ((for all N in L..I => (A(N) = 0)) and
           (for all N in IndexType =>
              (if N < L or N > I then A(N) = A'Loop_Entry(N))));
      -- Note it is not necessary to show that the vaule of U does not change
      -- within the loop.
      -- However 'Loop_Entry must be used rather than 'Old.
    end loop;
  end Clear;

end Loop_Entry;