SPARK 2005 to SPARK 2014 Mapping Specification
This appendix defines the mapping between SPARK 2005 and SPARK. It is intended as both a completeness check for the SPARK language design, and as a guide for projects upgrading from SPARK 2005 to SPARK 2014.
SPARK 2005 Features and SPARK 2014 Alternatives
Nearly every SPARK 2005 feature has a SPARK 2014 equivalent or there is an alternative way of providing the same feature in SPARK 2014. The only SPARK 2005 (not including RavenSPARK) features that do not have a direct alternative are:
the ‘Always_Valid attribute;
the ability to add pre and postconditions to an instantiation of a generic subprogram, e.g., Unchecked_Conversion; and
a precondition on the body of a subprogram refining the one on the specification - this is not usually required in SPARK 2014, it is normally replaced by the use of expression functions.
At the moment the first two features have to be accomplished using pragma Assume.
The following subsections of this appendix demonstrate how many SPARK 2005 idioms map into SPARK 2014. As a quick reference the table below shows, for each SPARK 2005 annotation or SPARK 2005 specific feature, a reference to the equivalent or alternative in SPARK 2014. In the table headings 2014 RM is the SPARK Reference Manual and Mapping is this appendix, the SPARK 2005 to SPARK 2014 mapping specification.
SPARK 2005 |
SPARK 2014 |
2014 RM |
Mapping |
---|---|---|---|
~ in post |
‘Old attribute - see Ada RM 6.1.1 |
||
~ in body |
‘Loop_Entry attribute |
||
<-> |
= |
||
A -> B |
(if A then B) - see Ada RM 4.5.7 |
||
% |
not needed |
||
always_valid |
not supported |
||
assert |
pragma Assert_And_Cut |
||
assert in loop |
pragma Loop_Invariant |
||
assume |
pragma Assume |
||
check |
pragma Assert - see Ada RM 11.4.2 |
||
derives on spec |
Depends aspect |
||
derives on body |
No separate spec - Depends aspect |
||
derives on body |
Separate spec - Refined_Depends aspect |
||
for all |
quantified_expression - see Ada RM 4.5.8 |
||
for some |
quantified_expression - See Ada RM 4.5.8 |
||
global on spec |
Global aspect |
||
global on body |
No separate spec - Global aspect |
||
global on body |
Separate spec - Refined_Global aspect |
||
hide |
pragma SPARK_Mode - see User Guide |
||
inherit |
not needed |
||
initializes |
Initializes aspect |
||
main_program |
not needed |
||
object assertions |
rule declarations are not needed |
||
own on spec |
Abstract_State aspect |
||
own on body |
Refined_State aspect |
||
post on spec |
postcondition - see Ada RM 6.1.1 |
||
post on body |
No separate spec - postcondition |
||
post on body |
Separate spec - Refined_Post aspect |
||
pre |
precondition - see Ada RM 6.1.1 |
||
proof functions |
Ghost functions |
||
proof types |
Ada types |
||
return |
‘Result attribute - see Ada RM 6.1.1 |
||
update |
delta aggregate |
Subprogram patterns
Global and Derives
This example demonstrates how global variables can be accessed through procedures/functions and presents how the SPARK 2005 derives annotation maps over to depends in SPARK 2014. The example consists of one procedure (Swap) and one function (Add). Swap accesses two global variables and swaps their contents while Add returns their sum.
Specification in SPARK 2005:
1package Swap_Add_05
2--# own X, Y: Integer;
3is
4 X, Y: Integer;
5
6 procedure Swap;
7 --# global in out X, Y;
8 --# derives X from Y &
9 --# Y from X;
10
11 function Add return Integer;
12 --# global in X, Y;
13
14end Swap_Add_05;
body in SPARK 2005:
1package body Swap_Add_05
2is
3 procedure Swap
4 is
5 Temporary: Integer;
6 begin
7 Temporary := X;
8 X := Y;
9 Y := Temporary;
10 end Swap;
11
12 function Add return Integer
13 is
14 begin
15 return X + Y;
16 end Add;
17
18end Swap_Add_05;
Specification in SPARK 2014:
1package Swap_Add_14
2 with SPARK_Mode
3is
4 -- Visible variables are not state abstractions.
5 X, Y: Integer;
6
7 procedure Swap
8 with Global => (In_Out => (X, Y)),
9 Depends => (X => Y, -- to be read as "X depends on Y"
10 Y => X); -- to be read as "Y depends on X"
11
12 function Add return Integer
13 with Global => (Input => (X, Y));
14end Swap_Add_14;
Body in SPARK 2014:
1package body Swap_Add_14
2 with SPARK_Mode
3is
4 procedure Swap is
5 Temporary: Integer;
6 begin
7 Temporary := X;
8 X := Y;
9 Y := Temporary;
10 end Swap;
11
12 function Add return Integer is (X + Y);
13end Swap_Add_14;
Pre/Post/Return contracts
This example demonstrates how the Pre/Post/Return contracts are restructured and how they map from SPARK 2005 to SPARK 2014. Procedure Swap and function Add perform the same task as in the previous example, but the global variables have been replaced by parameters (this is not necessarry for proof) and they have been augmented by pre and post annotations. Two additional functions (Max and Divide) and one additional procedure (Swap_Array_Elements) have also been included in this example in order to demonstrate further features. Max returns the maximum of the two parameters. Divide returns the division of the two parameters after having ensured that the divisor is not equal to zero. The Swap_Array_Elements procedure swaps the contents of two elements of an array.
Specification in SPARK 2005:
1package Swap_Add_Max_05 is
2
3 subtype Index is Integer range 1..100;
4 type Array_Type is array (Index) of Integer;
5
6 procedure Swap (X, Y : in out Integer);
7 --# post X = Y~ and Y = X~;
8
9 function Add (X, Y : Integer) return Integer;
10 --# pre ((X >= 0 and Y >= 0) -> (X + Y <= Integer'Last)) and
11 --# ((X < 0 and Y < 0) -> (X + Y >= Integer'First));
12 --# return X + Y;
13
14 function Max (X, Y : Integer) return Integer;
15 --# return Z => (X >= Y -> Z = X) and
16 --# (Y > X -> Z = Y);
17
18 function Divide (X, Y : Integer) return Integer;
19 --# pre Y /= 0 and X > Integer'First;
20 --# return X / Y;
21
22 procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type);
23 --# post A = A~[I => A~(J); J => A~(I)];
24
25end Swap_Add_Max_05;
Body in SPARK 2005:
1package body Swap_Add_Max_05
2is
3 procedure Swap (X, Y: in out Integer)
4 is
5 Temporary: Integer;
6 begin
7 Temporary := X;
8 X := Y;
9 Y := Temporary;
10 end Swap;
11
12 function Add (X, Y : Integer) return Integer
13 is
14 begin
15 return X + Y;
16 end Add;
17
18 function Max (X, Y : Integer) return Integer
19 is
20 Result: Integer;
21 begin
22 if X >= Y then
23 Result := X;
24 else
25 Result := Y;
26 end if;
27 return Result;
28 end Max;
29
30 function Divide (X, Y : Integer) return Integer
31 is
32 begin
33 return X / Y;
34 end Divide;
35
36 procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type)
37 is
38 Temporary: Integer;
39 begin
40 Temporary := A(I);
41 A(I) := A(J);
42 A(J) := Temporary;
43 end Swap_Array_Elements;
44
45end Swap_Add_Max_05;
Specification in SPARK 2014:
1package Swap_Add_Max_14
2 with SPARK_Mode
3is
4 subtype Index is Integer range 1..100;
5 type Array_Type is array (Index) of Integer;
6
7 procedure Swap (X, Y : in out Integer)
8 with Post => (X = Y'Old and Y = X'Old);
9
10 function Add (X, Y : Integer) return Integer
11 with Pre => (if X >= 0 and Y >= 0 then X <= Integer'Last - Y
12 elsif X < 0 and Y < 0 then X >= Integer'First - Y),
13 -- The precondition may be written as X + Y in Integer if
14 -- an extended arithmetic mode is selected
15 Post => Add'Result = X + Y;
16
17 function Max (X, Y : Integer) return Integer
18 with Post => Max'Result = (if X >= Y then X else Y);
19
20 function Divide (X, Y : Integer) return Integer
21 with Pre => Y /= 0 and X > Integer'First,
22 Post => Divide'Result = X / Y;
23
24 procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type)
25 with Post => A = A'Old'Update (I => A'Old (J),
26 J => A'Old (I));
27end Swap_Add_Max_14;
Body in SPARK 2014:
1package body Swap_Add_Max_14
2 with SPARK_Mode
3is
4 procedure Swap (X, Y : in out Integer) is
5 Temporary: Integer;
6 begin
7 Temporary := X;
8 X := Y;
9 Y := Temporary;
10 end Swap;
11
12 function Add (X, Y : Integer) return Integer is (X + Y);
13
14 function Max (X, Y : Integer) return Integer is
15 (if X >= Y then X
16 else Y);
17
18 function Divide (X, Y : Integer) return Integer is (X / Y);
19
20 procedure Swap_Array_Elements(I, J : Index; A: in out Array_Type) is
21 Temporary: Integer;
22 begin
23 Temporary := A(I);
24 A(I) := A(J);
25 A(J) := Temporary;
26 end Swap_Array_Elements;
27end Swap_Add_Max_14;
Attributes of unconstrained out parameter in precondition
The following example illustrates the fact that the attributes of an unconstrained formal array parameter of mode “out” are permitted to appear in a precondition. The flow analyzer also needs to be smart about this, since it knows that X’First and X’Last are well-defined in the body, even though the content of X is not.
Specification in SPARK 2005:
1package P
2is
3 type A is array (Positive range <>) of Integer;
4
5 -- Shows that X'First and X'Last _can_ be used in
6 -- precondition here, even though X is mode "out"...
7 procedure Init (X : out A);
8 --# pre X'First = 1 and
9 --# X'Last >= 20;
10 --# post for all I in Positive range X'Range =>
11 --# ((I /= 20 -> (X (I) = 0)) and
12 --# (I = 1 -> (X (I) = X'Last)) and
13 --# (I = 20 -> (X (I) = -1)));
14
15end P;
Body in SPARK 2005:
1package body P is
2
3 procedure Init (X : out A) is
4 begin
5 X := (others => 0);
6 X (1) := X'Last;
7 X (20) := -1;
8 end Init;
9
10end P;
Specification in SPARK 2014:
1package P
2 with SPARK_Mode
3is
4 type A is array (Positive range <>) of Integer;
5
6 -- Shows that X'First, X'Last and X'Length _can_ be used
7 -- in precondition here, even though X is mode "out"...
8 procedure Init (X : out A)
9 with Pre => X'First = 1 and X'Last >= 20,
10 Post => (for all I in X'Range =>
11 (if I = 1 then X (I) = X'Last
12 elsif I = 20 then X (I) = -1
13 else X (I) = 0));
14end P;
Body in SPARK 2014:
1package body P
2 with SPARK_Mode
3is
4 procedure Init (X : out A) is
5 begin
6 X := (1 => X'Last, 20 => -1, others => 0);
7 end Init;
8end P;
Data Abstraction, Refinement and Initialization
This example demonstrates data abstraction and refinement. It also shows how abstract data is shown to be initialized during package elaboration (it need not be - it could be initialized through an explicit subprogram call, in which case the Initalizes annotation should not be given). There is also a demonstration of how procedures and functions can be nested within other procedures and functions. Furthermore, it illustrates how global variable refinement can be performed.
Specification in SPARK 2005:
1package Nesting_Refinement_05
2--# own State;
3--# initializes State;
4is
5 procedure Operate_On_State;
6 --# global in out State;
7end Nesting_Refinement_05;
Body in SPARK 2005:
1package body Nesting_Refinement_05
2--# own State is X, Y; -- Refined State
3is
4 X, Y: Integer;
5
6 procedure Operate_On_State
7 --# global in out X; -- Refined Global
8 --# out Y;
9 is
10 Z: Integer;
11
12 procedure Add_Z_To_X
13 --# global in out X;
14 --# in Z;
15 is
16 begin
17 X := X + Z;
18 end Add_Z_To_X;
19
20 procedure Overwrite_Y_With_Z
21 --# global out Y;
22 --# in Z;
23 is
24 begin
25 Y := Z;
26 end Overwrite_Y_With_Z;
27 begin
28 Z := 5;
29 Add_Z_To_X;
30 Overwrite_Y_With_Z;
31 end Operate_On_State;
32
33begin -- Promised to initialize State
34 -- (which consists of X and Y)
35 X := 10;
36 Y := 20;
37end Nesting_Refinement_05;
Specification in SPARK 2014:
1package Nesting_Refinement_14
2 with SPARK_Mode,
3 Abstract_State => State,
4 Initializes => State
5is
6 procedure Operate_On_State
7 with Global => (In_Out => State);
8end Nesting_Refinement_14;
Body in SPARK 2014:
1package body Nesting_Refinement_14
2 -- State is refined onto two concrete variables X and Y
3 with SPARK_Mode,
4 Refined_State => (State => (X, Y))
5is
6 X, Y: Integer;
7
8 procedure Operate_On_State
9 with Refined_Global => (In_Out => X,
10 Output => Y)
11 is
12 Z: Integer;
13
14 procedure Add_Z_To_X
15 with Global => (In_Out => X,
16 Input => Z)
17 is
18 begin
19 X := X + Z;
20 end Add_Z_To_X;
21
22 procedure Overwrite_Y_With_Z
23 with Global => (Output => Y,
24 Input => Z)
25 is
26 begin
27 Y := Z;
28 end Overwrite_Y_With_Z;
29 begin
30 Z := 5;
31 Add_Z_To_X;
32 Overwrite_Y_With_Z;
33 end Operate_On_State;
34
35begin
36 -- Promised to initialize State
37 -- (which consists of X and Y)
38 X := 10;
39 Y := 20;
40end Nesting_Refinement_14;
Package patterns
Abstract Data Types (ADTs)
Visible type
The following example adds no mapping information. The SPARK 2005 and SPARK 2014 versions of the code are identical. Only the specification of the SPARK 2005 code will be presented. The reason why this code is being provided is to allow for a comparison between a package that is purely public and an equivalent one that also has private elements.
Specification in SPARK 2005:
1package Stacks_05 is
2 Stack_Size : constant := 100;
3 type Pointer_Range is range 0 .. Stack_Size;
4 subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
5 type Vector is array(Index_Range) of Integer;
6
7 type Stack is
8 record
9 Stack_Vector : Vector;
10 Stack_Pointer : Pointer_Range;
11 end record;
12
13 function Is_Empty(S : Stack) return Boolean;
14 function Is_Full(S : Stack) return Boolean;
15
16 procedure Clear(S : out Stack);
17 procedure Push(S : in out Stack; X : in Integer);
18 procedure Pop(S : in out Stack; X : out Integer);
19end Stacks_05;
Private type
Similarly to the previous example, this one does not contain any annotations either. Due to this, the SPARK 2005 and SPARK 2014 versions are exactly the same. Only the specification of the 2005 version shall be presented.
Specification in SPARK 2005:
1package Stacks_05 is
2
3 type Stack is private;
4
5 function Is_Empty(S : Stack) return Boolean;
6 function Is_Full(S : Stack) return Boolean;
7
8 procedure Clear(S : out Stack);
9 procedure Push(S : in out Stack; X : in Integer);
10 procedure Pop(S : in out Stack; X : out Integer);
11
12private
13 Stack_Size : constant := 100;
14 type Pointer_Range is range 0 .. Stack_Size;
15 subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
16 type Vector is array(Index_Range) of Integer;
17
18 type Stack is
19 record
20 Stack_Vector : Vector;
21 Stack_Pointer : Pointer_Range;
22 end record;
23end Stacks_05;
Private type with pre/post contracts
This example demonstrates how pre and post conditions of subprograms may be specified in terms of functions declared in the same package specification. The function declarations are completed in the body and the postconditions of the completed functions are used to prove the implementations of the other subprograms. In SPARK 2014 explicit postconditions do not have to be specified on the bodies of the functions as they are implemented as expression functions and the expression, E, of the function acts as a default refined postcondition, i.e., F’Result = E. Note that the SPARK 2014 version is proven entirely automatically whereas the SPARK 2005 version requires user defined proof rules.
Specification in SPARK 2005:
1package Stacks_05
2is
3
4 type Stack is private;
5
6 function Is_Empty(S : Stack) return Boolean;
7 function Is_Full(S : Stack) return Boolean;
8
9 procedure Clear(S : in out Stack);
10 --# post Is_Empty(S);
11 procedure Push(S : in out Stack; X : in Integer);
12 --# pre not Is_Full(S);
13 --# post not Is_Empty(S);
14 procedure Pop(S : in out Stack; X : out Integer);
15 --# pre not Is_Empty(S);
16 --# post not Is_Full(S);
17
18private
19 Stack_Size : constant := 100;
20 type Pointer_Range is range 0 .. Stack_Size;
21 subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
22 type Vector is array(Index_Range) of Integer;
23
24 type Stack is
25 record
26 Stack_Vector : Vector;
27 Stack_Pointer : Pointer_Range;
28 end record;
29end Stacks_05;
Body in SPARK 2005:
1package body Stacks_05 is
2
3 function Is_Empty (S : Stack) return Boolean
4 --# return S.Stack_Pointer = 0;
5 is
6 begin
7 return S.Stack_Pointer = 0;
8 end Is_Empty;
9
10 function Is_Full (S : Stack) return Boolean
11 --# return S.Stack_Pointer = Stack_Size;
12 is
13 begin
14 return S.Stack_Pointer = Stack_Size;
15 end Is_Full;
16
17 procedure Clear (S : in out Stack)
18 --# post Is_Empty(S);
19 is
20 begin
21 S.Stack_Pointer := 0;
22 end Clear;
23
24 procedure Push (S : in out Stack; X : in Integer)
25 is
26 begin
27 S.Stack_Pointer := S.Stack_Pointer + 1;
28 S.Stack_Vector (S.Stack_Pointer) := X;
29 end Push;
30
31 procedure Pop (S : in out Stack; X : out Integer)
32 is
33 begin
34 X := S.Stack_Vector (S.Stack_Pointer);
35 S.Stack_Pointer := S.Stack_Pointer - 1;
36 end Pop;
37end Stacks_05;
Specification in SPARK 2014:
1package Stacks_14
2 with SPARK_Mode
3is
4 type Stack is private;
5
6 function Is_Empty(S : Stack) return Boolean;
7 function Is_Full(S : Stack) return Boolean;
8
9 procedure Clear(S : in out Stack)
10 with Post => Is_Empty(S);
11
12 procedure Push(S : in out Stack; X : in Integer)
13 with Pre => not Is_Full(S),
14 Post => not Is_Empty(S);
15
16 procedure Pop(S : in out Stack; X : out Integer)
17 with Pre => not Is_Empty(S),
18 Post => not Is_Full(S);
19
20private
21 Stack_Size : constant := 100;
22 type Pointer_Range is range 0 .. Stack_Size;
23 subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
24 type Vector is array(Index_Range) of Integer;
25
26 type Stack is record
27 Stack_Vector : Vector;
28 Stack_Pointer : Pointer_Range;
29 end record;
30end Stacks_14;
Body in SPARK 2014:
1package body Stacks_14
2 with SPARK_Mode
3is
4 -- Expression function has default refined postcondition of
5 -- Is_Empty'Result = (S.Stack_Pointer = 0)
6 function Is_Empty(S : Stack) return Boolean is (S.Stack_Pointer = 0);
7
8 -- Expression function has default refined postcondition of
9 -- Is_Empty'Result = (S.Stack_Pointer = Stack_Size)
10 function Is_Full(S : Stack) return Boolean is (S.Stack_Pointer = Stack_Size);
11
12 procedure Clear(S : in out Stack) is
13 begin
14 S.Stack_Pointer := 0;
15 end Clear;
16
17 procedure Push(S : in out Stack; X : in Integer) is
18 begin
19 S.Stack_Pointer := S.Stack_Pointer + 1;
20 S.Stack_Vector(S.Stack_Pointer) := X;
21 end Push;
22
23 procedure Pop(S : in out Stack; X : out Integer) is
24 begin
25 X := S.Stack_Vector(S.Stack_Pointer);
26 S.Stack_Pointer := S.Stack_Pointer - 1;
27 end Pop;
28end Stacks_14;
Private/Public child visibility
The following example demonstrates visibility rules that apply between public children, private children and their parent in SPARK 2005. More specifically, it shows that:
Private children are able to see their private siblings but not their public siblings.
Public children are able to see their public siblings but not their private siblings.
All children have access to their parent but the parent can only access private children.
Applying the SPARK tools on the following files will produce certain errors. This was intentionally done in order to illustrate both legal and illegal access attempts.
SPARK 2014 shares Ada’s visibility rules. No restrictions have been applied in terms of visibility. Note that SPARK 2014 code does not require Inherit annotations.
Specification of parent in SPARK 2005:
1package Parent_05
2is
3 function F (X : Integer) return Integer;
4 function G (X : Integer) return Integer;
5end Parent_05;
Specification of private child A in SPARK 2005:
1--#inherit Parent_05; -- OK
2private package Parent_05.Private_Child_A_05
3is
4 function F (X : Integer) return Integer;
5end Parent_05.Private_Child_A_05;
Specification of private child B in SPARK 2005:
1--#inherit Parent_05.Private_Child_A_05, -- OK
2--# Parent_05.Public_Child_A_05; -- error, public sibling
3private package Parent_05.Private_Child_B_05
4is
5 function H (X : Integer) return Integer;
6end Parent_05.Private_Child_B_05;
Specification of public child A in SPARK 2005:
1--#inherit Parent_05, -- OK
2--# Parent_05.Private_Child_A_05; -- error, private sibling
3package Parent_05.Public_Child_A_05
4is
5 function G (X : Integer) return Integer;
6end Parent_05.Public_Child_A_05;
Specification of public child B in SPARK 2005:
1--#inherit Parent_05.Public_Child_A_05; -- OK
2package Parent_05.Public_Child_B_05
3is
4 function H (X : Integer) return Integer;
5end Parent_05.Public_Child_B_05;
Body of parent in SPARK 2005:
1with Parent_05.Private_Child_A_05, -- OK
2 Parent_05.Public_Child_A_05; -- error, public children not visible
3package body Parent_05
4is
5 function F (X : Integer) return Integer is
6 begin
7 return Private_Child_A_05.F (X);
8 end F;
9
10 function G (X : Integer) return Integer is
11 begin
12 return Public_Child_A_05.G (X);
13 end G;
14
15end Parent_05;
Body of public child A in SPARK 2005:
1package body Parent_05.Public_Child_A_05
2is
3 function G (X : Integer) return Integer is
4 Result : Integer;
5 begin
6 if X <= 0 then
7 Result := 0;
8 else
9 Result := Parent_05.F (X); -- OK
10 end if;
11 return Result;
12 end G;
13end Parent_05.Public_Child_A_05;
Body of public child B in SPARK 2005:
1with Parent_05.Private_Child_B_05;
2package body Parent_05.Public_Child_B_05
3is
4 function H (X : Integer) return Integer is
5 begin
6 return Parent_05.Private_Child_B_05.H (X);
7 end H;
8end Parent_05.Public_Child_B_05;
Body of private child B in SPARK 2005:
1package body Parent_05.Private_Child_B_05
2is
3 function H (X : Integer) return Integer is
4 Result : Integer;
5 begin
6 if X <= 10 then
7 Result := 10;
8 else
9 Result := Parent_05.F (X); -- Illegal in SPARK 2005
10 end if;
11 return Result;
12 end H;
13end Parent_05.Private_Child_B_05;
Specification of parent in SPARK 2014:
1package Parent_14
2 with SPARK_Mode
3is
4 function F (X : Integer) return Integer;
5 function G (X : Integer) return Integer;
6end Parent_14;
Specification of private child A in SPARK 2014:
1private package Parent_14.Private_Child_A_14
2 with SPARK_Mode
3is
4 function F (X : Integer) return Integer
5 with Global => null;
6end Parent_14.Private_Child_A_14;
Specification of private child B in SPARK 2014:
1private package Parent_14.Private_Child_B_14
2 with SPARK_Mode
3is
4 function H (X : Integer) return Integer;
5end Parent_14.Private_Child_B_14;
Specification of public child A in SPARK 2014:
1package Parent_14.Public_Child_A_14
2 with SPARK_Mode
3is
4 function G (X : Integer) return Integer;
5end Parent_14.Public_Child_A_14;
Specification of public child B in SPARK 2014:
1package Parent_14.Public_Child_B_14
2 with SPARK_Mode
3is
4 function H (X : Integer) return Integer;
5end Parent_14.Public_Child_B_14;
Body of parent in SPARK 2014:
1with Parent_14.Private_Child_A_14, -- OK
2 Parent_14.Public_Child_A_14; -- OK
3
4package body Parent_14
5 with SPARK_Mode
6is
7 function F (X : Integer) return Integer is (Private_Child_A_14.F (X));
8
9 function G (X : Integer) return Integer is (Public_Child_A_14.G (X));
10end Parent_14;
Body of public child A in SPARK 2014:
1package body Parent_14.Public_Child_A_14
2 with SPARK_Mode
3is
4 function G (X : Integer) return Integer is
5 (if X <= 0 then 0
6 else Parent_14.F (X)); -- OK
7end Parent_14.Public_Child_A_14;
Body of public child B in SPARK 2014:
1with Parent_14.Private_Child_B_14;
2
3package body Parent_14.Public_Child_B_14
4 with SPARK_Mode
5is
6 function H (X : Integer) return Integer is
7 (Parent_14.Private_Child_B_14.H (X));
8end Parent_14.Public_Child_B_14;
Body of private child B in SPARK 2014:
1package body Parent_14.Private_Child_B_14
2 with SPARK_Mode
3is
4 function H (X : Integer) return Integer is
5 (if X <= 10 then 10
6 else Parent_14.F (X)); -- Legal in SPARK 2014
7end Parent_14.Private_Child_B_14;
Abstract State Machines (ASMs)
Visible, concrete state
Initialized by declaration
The example that follows presents a way in SPARK 2005 of initializing a concrete own variable (a state that is not refined) at the point of the declaration of the variables that compose it. Generally it is not good practice to declare several concrete own variables, data abstraction should be used but here we are doing it for the point of illustration.
In SPARK 2014 the client’s view of package state is either visible (declared in the visible part of the package) or a state abstraction representing hidden state. A variable cannot overload the name of a state abstraction and therefore a state abstraction must be completed by a refinement given in the body of the package - there is no concept of a concrete state abstraction. The constituents of a state abstraction may be initialized at their declaration.
Specification in SPARK 2005:
1package Stack_05
2--# own S, Pointer; -- concrete state
3--# initializes S, Pointer;
4is
5 procedure Push(X : in Integer);
6 --# global in out S, Pointer;
7
8 procedure Pop(X : out Integer);
9 --# global in S; in out Pointer;
10end Stack_05;
Body in SPARK 2005:
1package body Stack_05
2is
3 Stack_Size : constant := 100;
4 type Pointer_Range is range 0 .. Stack_Size;
5 subtype Index_Range is Pointer_Range range 1..Stack_Size;
6 type Vector is array(Index_Range) of Integer;
7
8 S : Vector := Vector'(Index_Range => 0); -- Initialization of S
9 Pointer : Pointer_Range := 0; -- Initialization of Pointer
10
11 procedure Push(X : in Integer)
12 is
13 begin
14 Pointer := Pointer + 1;
15 S(Pointer) := X;
16 end Push;
17
18 procedure Pop(X : out Integer)
19 is
20 begin
21 X := S(Pointer);
22 Pointer := Pointer - 1;
23 end Pop;
24
25end Stack_05;
Specification in SPARK 2014:
1package Stack_14
2 with SPARK_Mode,
3 Abstract_State => (S_State, Pointer_State),
4 Initializes => (S_State, Pointer_State)
5is
6 procedure Push(X : in Integer)
7 with Global => (In_Out => (S_State, Pointer_State));
8
9 procedure Pop(X : out Integer)
10 with Global => (Input => S_State,
11 In_Out => Pointer_State);
12end Stack_14;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (S_State => S,
4 Pointer_State => Pointer)
5is
6 Stack_Size : constant := 100;
7 type Pointer_Range is range 0 .. Stack_Size;
8 subtype Index_Range is Pointer_Range range 1..Stack_Size;
9 type Vector is array(Index_Range) of Integer;
10
11 S : Vector := Vector'(Index_Range => 0); -- Initialization of S
12 Pointer : Pointer_Range := 0; -- Initialization of Pointer
13
14 procedure Push (X : in Integer)
15 with Refined_Global => (In_Out => (S, Pointer))
16 is
17 begin
18 Pointer := Pointer + 1;
19 S (Pointer) := X;
20 end Push;
21
22 procedure Pop(X : out Integer)
23 with Refined_Global => (Input => S,
24 In_Out => Pointer)
25 is
26 begin
27 X := S (Pointer);
28 Pointer := Pointer - 1;
29 end Pop;
30end Stack_14;
Initialized by elaboration
The following example presents how a package’s concrete state can be initialized at the statements section of the body. The specifications of both SPARK 2005 and SPARK 2014 are not presented since they are identical to the specifications of the previous example.
Body in SPARK 2005:
1package body Stack_05
2is
3 Stack_Size : constant := 100;
4 type Pointer_Range is range 0 .. Stack_Size;
5 subtype Index_Range is Pointer_Range range 1..Stack_Size;
6 type Vector is array(Index_Range) of Integer;
7
8 S : Vector;
9 Pointer : Pointer_Range;
10
11 procedure Push(X : in Integer)
12 is
13 begin
14 Pointer := Pointer + 1;
15 S(Pointer) := X;
16 end Push;
17
18 procedure Pop(X : out Integer)
19 is
20 begin
21 X := S(Pointer);
22 Pointer := Pointer - 1;
23 end Pop;
24
25begin -- initialization
26 Pointer := 0;
27 S := Vector'(Index_Range => 0);
28end Stack_05;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (S_State => S,
4 Pointer_State => Pointer)
5is
6 Stack_Size : constant := 100;
7 type Pointer_Range is range 0 .. Stack_Size;
8 subtype Index_Range is Pointer_Range range 1..Stack_Size;
9 type Vector is array(Index_Range) of Integer;
10
11 S : Vector;
12 Pointer : Pointer_Range;
13
14 procedure Push (X : in Integer)
15 with Refined_Global => (In_Out => (S, Pointer))
16 is
17 begin
18 Pointer := Pointer + 1;
19 S (Pointer) := X;
20 end Push;
21
22 procedure Pop(X : out Integer)
23 with Refined_Global => (Input => S,
24 In_Out => Pointer)
25 is
26 begin
27 X := S (Pointer);
28 Pointer := Pointer - 1;
29 end Pop;
30begin
31 -- initialization
32 Pointer := 0;
33 S := Vector'(Index_Range => 0);
34end Stack_14;
Private, concrete state
In SPARK 2005 variables declared in the private part of a package are considered to be concrete own variables. In SPARK 2014 they are hidden state and must be constituents of a state abstraction.
The SPARK 2005 body has not been included since it does not contain any annotations.
Specification in SPARK 2005:
1package Stack_05
2--# own S, Pointer;
3is
4 procedure Push(X : in Integer);
5 --# global in out S, Pointer;
6
7 procedure Pop(X : out Integer);
8 --# global in S;
9 --# in out Pointer;
10private
11 Stack_Size : constant := 100;
12 type Pointer_Range is range 0 .. Stack_Size;
13 subtype Index_Range is Pointer_Range range 1..Stack_Size;
14 type Vector is array(Index_Range) of Integer;
15
16 S : Vector;
17 Pointer : Pointer_Range;
18end Stack_05;
Specification in SPARK 2014:
1package Stack_14
2 with SPARK_Mode,
3 Abstract_State => (S_State, Pointer_State)
4is
5 procedure Push(X : in Integer)
6 with Global => (In_Out => (S_State, Pointer_State));
7
8 procedure Pop(X : out Integer)
9 with Global => (Input => S_State,
10 In_Out => Pointer_State);
11
12private
13 Stack_Size : constant := 100;
14 type Pointer_Range is range 0 .. Stack_Size;
15 subtype Index_Range is Pointer_Range range 1..Stack_Size;
16 type Vector is array(Index_Range) of Integer;
17
18 S : Vector with Part_Of => S_State;
19 Pointer : Pointer_Range with Part_Of => Pointer_State;
20end Stack_14;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (S_State => S,
4 Pointer_State => Pointer)
5is
6 procedure Push(X : in Integer)
7 with Refined_Global => (In_Out => (S, Pointer))
8 is
9 begin
10 Pointer := Pointer + 1;
11 S (Pointer) := X;
12 end Push;
13
14 procedure Pop (X : out Integer)
15 with Refined_Global => (Input => S,
16 In_Out => Pointer)
17 is
18 begin
19 X := S (Pointer);
20 Pointer := Pointer - 1;
21 end Pop;
22end Stack_14;
Private, abstract state, refining onto concrete states in body
Initialized by procedure call
In this example, the abstract state declared at the specification is refined at the body. Procedure Init can be invoked by users of the package, in order to initialize the state.
Specification in SPARK 2005:
1package Stack_05
2--# own State;
3is
4 procedure Push(X : in Integer);
5 --# global in out State;
6
7 procedure Pop(X : out Integer);
8 --# global in out State;
9
10 procedure Init;
11 --# global out State;
12
13end Stack_05;
Body in SPARK 2005:
1package body Stack_05
2--# own State is S, Pointer;
3is
4 Stack_Size : constant := 100;
5 type Pointer_Range is range 0 .. Stack_Size;
6 subtype Index_Range is Pointer_Range range 1..Stack_Size;
7 type Vector is array(Index_Range) of Integer;
8
9 Pointer : Pointer_Range;
10 S : Vector;
11
12 procedure Push(X : in Integer)
13 --# global in out Pointer, S;
14 is
15 begin
16 Pointer := Pointer + 1;
17 S(Pointer) := X;
18 end Push;
19
20 procedure Pop(X : out Integer)
21 --# global in S;
22 --# in out Pointer;
23 is
24 begin
25 X := S(Pointer);
26 Pointer := Pointer - 1;
27 end Pop;
28
29 procedure Init
30 --# global out Pointer, S;
31 is
32 begin
33 Pointer := 0;
34 S := Vector'(Index_Range => 0);
35 end Init;
36end Stack_05;
Specification in SPARK 2014:
1package Stack_14
2 with SPARK_Mode,
3 Abstract_State => State
4is
5 procedure Push(X : in Integer)
6 with Global => (In_Out => State);
7
8 procedure Pop(X : out Integer)
9 with Global => (In_Out => State);
10
11 procedure Init
12 with Global => (Output => State);
13end Stack_14;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (State => (Pointer, S))
4is
5 Stack_Size : constant := 100;
6 type Pointer_Range is range 0 .. Stack_Size;
7 subtype Index_Range is Pointer_Range range 1..Stack_Size;
8 type Vector is array(Index_Range) of Integer;
9
10 Pointer : Pointer_Range;
11 S : Vector;
12
13 procedure Push(X : in Integer)
14 with Refined_Global => (In_Out => (Pointer, S))
15 is
16 begin
17 Pointer := Pointer + 1;
18 S (Pointer) := X;
19 end Push;
20
21 procedure Pop (X : out Integer)
22 with Refined_Global => (In_Out => Pointer,
23 Input => S)
24 is
25 begin
26 X := S (Pointer);
27 Pointer := Pointer - 1;
28 end Pop;
29
30 procedure Init
31 with Refined_Global => (Output => (Pointer, S))
32 is
33 begin
34 Pointer := 0;
35 S := (Index_Range => 0);
36 end Init;
37end Stack_14;
Initialized by elaboration of declaration
The example that follows introduces an abstract state at the specification and refines it at the body. The constituents of the abstract state are initialized at declaration.
Specification in SPARK 2005:
1package Stack_05
2--# own State;
3--# initializes State;
4is
5 procedure Push(X : in Integer);
6 --# global in out State;
7
8 procedure Pop(X : out Integer);
9 --# global in out State;
10
11end Stack_05;
Body in SPARK 2005:
1package body Stack_05
2--# own State is Pointer, S; -- refinement of state
3is
4 Stack_Size : constant := 100;
5 type Pointer_Range is range 0 .. Stack_Size;
6 subtype Index_Range is Pointer_Range range 1..Stack_Size;
7 type Vector is array(Index_Range) of Integer;
8
9 S : Vector := Vector'(others => 0);
10 Pointer : Pointer_Range := 0;
11 -- initialization by elaboration of declaration
12
13 procedure Push(X : in Integer)
14 --# global in out Pointer, S;
15 is
16 begin
17 Pointer := Pointer + 1;
18 S(Pointer) := X;
19 end Push;
20
21 procedure Pop(X : out Integer)
22 --# global in S;
23 --# in out Pointer;
24 is
25 begin
26 X := S(Pointer);
27 Pointer := Pointer - 1;
28 end Pop;
29end Stack_05;
Specification in SPARK 2014:
1package Stack_14
2 with SPARK_Mode,
3 Abstract_State => State,
4 Initializes => State
5is
6 procedure Push(X : in Integer)
7 with Global => (In_Out => State);
8
9 procedure Pop(X : out Integer)
10 with Global => (In_Out => State);
11end Stack_14;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (State => (Pointer, S)) -- refinement of state
4is
5 Stack_Size : constant := 100;
6 type Pointer_Range is range 0 .. Stack_Size;
7 subtype Index_Range is Pointer_Range range 1..Stack_Size;
8 type Vector is array(Index_Range) of Integer;
9
10 S : Vector := (others => 0);
11 Pointer : Pointer_Range := 0;
12 -- initialization by elaboration of declaration
13
14 procedure Push(X : in Integer)
15 with Refined_Global => (In_Out => (Pointer, S))
16 is
17 begin
18 Pointer := Pointer + 1;
19 S (Pointer) := X;
20 end Push;
21
22 procedure Pop(X : out Integer)
23 with Refined_Global => (In_Out => Pointer,
24 Input => S)
25 is
26 begin
27 X := S (Pointer);
28 Pointer := Pointer - 1;
29 end Pop;
30end Stack_14;
Initialized by package body statements
This example introduces an abstract state at the specification and refines it at the body. The constituents of the abstract state are initialized at the statements part of the body. The specifications of the SPARK 2005 and SPARK 2014 versions of the code are as in the previous example and have thus not been included.
Body in SPARK 2005:
1package body Stack_05
2--# own State is Pointer, S; -- refinement of state
3is
4 Stack_Size : constant := 100;
5 type Pointer_Range is range 0 .. Stack_Size;
6 subtype Index_Range is Pointer_Range range 1..Stack_Size;
7 type Vector is array(Index_Range) of Integer;
8
9 S : Vector;
10 Pointer : Pointer_Range;
11
12 procedure Push(X : in Integer)
13 --# global in out Pointer, S;
14 is
15 begin
16 Pointer := Pointer + 1;
17 S(Pointer) := X;
18 end Push;
19
20 procedure Pop(X : out Integer)
21 --# global in out Pointer;
22 --# in S;
23 is
24 begin
25 X := S(Pointer);
26 Pointer := Pointer - 1;
27 end Pop;
28begin -- initialized by package body statements
29 Pointer := 0;
30 S := Vector'(Index_Range => 0);
31end Stack_05;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (State => (Pointer, S)) -- refinement of state
4is
5 Stack_Size : constant := 100;
6 type Pointer_Range is range 0 .. Stack_Size;
7 subtype Index_Range is Pointer_Range range 1..Stack_Size;
8 type Vector is array(Index_Range) of Integer;
9
10 S : Vector;
11 Pointer : Pointer_Range;
12
13 procedure Push(X : in Integer)
14 with Refined_Global => (In_Out => (Pointer, S))
15 is
16 begin
17 Pointer := Pointer + 1;
18 S (Pointer) := X;
19 end Push;
20
21 procedure Pop(X : out Integer)
22 with Refined_Global => (In_Out => Pointer,
23 Input => S)
24 is
25 begin
26 X := S (Pointer);
27 Pointer := Pointer - 1;
28 end Pop;
29begin
30 -- initialized by package body statements
31 Pointer := 0;
32 S := (Index_Range => 0);
33end Stack_14;
Initialized by mixture of declaration and statements
This example introduces an abstract state at the specification and refines it at the body. Some of the constituents of the abstract state are initialized during their declaration and the rest at the statements part of the body.
Specification in SPARK 2005:
1package Stack_05
2--# own Stack;
3--# initializes Stack;
4is
5 procedure Push(X : in Integer);
6 --# global in out Stack;
7
8 procedure Pop(X : out Integer);
9 --# global in out Stack;
10
11end Stack_05;
Body in SPARK 2005:
1package body Stack_05
2--# own Stack is S, Pointer; -- state refinement
3is
4 Stack_Size : constant := 100;
5 type Pointer_Range is range 0 .. Stack_Size;
6 subtype Index_Range is Pointer_Range range 1..Stack_Size;
7 type Vector is array(Index_Range) of Integer;
8 S : Vector;
9
10 Pointer : Pointer_Range := 0;
11 -- initialization by elaboration of declaration
12
13 procedure Push(X : in Integer)
14 --# global in out S, Pointer;
15 is
16 begin
17 Pointer := Pointer + 1;
18 S(Pointer) := X;
19 end Push;
20
21 procedure Pop(X : out Integer)
22 --# global in S;
23 --# in out Pointer;
24 is
25 begin
26 X := S(Pointer);
27 Pointer := Pointer - 1;
28 end Pop;
29begin -- initialization by body statements
30 S := Vector'(Index_Range => 0);
31end Stack_05;
Specification in SPARK 2014:
1package Stack_14
2 with SPARK_Mode,
3 Abstract_State => Stack,
4 Initializes => Stack
5is
6 procedure Push(X : in Integer)
7 with Global => (In_Out => Stack);
8
9 procedure Pop(X : out Integer)
10 with Global => (In_Out => Stack);
11end Stack_14;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (Stack => (S, Pointer)) -- state refinement
4is
5 Stack_Size : constant := 100;
6 type Pointer_Range is range 0 .. Stack_Size;
7 subtype Index_Range is Pointer_Range range 1..Stack_Size;
8 type Vector is array(Index_Range) of Integer;
9
10 S : Vector; -- left uninitialized
11 Pointer : Pointer_Range := 0;
12 -- initialization by elaboration of declaration
13
14 procedure Push(X : in Integer)
15 with Refined_Global => (In_Out => (S, Pointer))
16 is
17 begin
18 Pointer := Pointer + 1;
19 S (Pointer) := X;
20 end Push;
21
22 procedure Pop (X : out Integer)
23 with Refined_Global => (Input => S,
24 In_Out => Pointer)
25 is
26 begin
27 X := S (Pointer);
28 Pointer := Pointer - 1;
29 end Pop;
30begin
31 -- partial initialization by body statements
32 S := (Index_Range => 0);
33end Stack_14;
Initial condition
This example introduces a new SPARK 2014 feature that did not exist in SPARK 2005. On top of declaring an abstract state and promising to initialize it, we also illustrate certain conditions that will be valid after initialization. There is a verification condition to show that immediately after the elaboration of the package that the specified Initial_Condition is True. Checks will be generated that have to be proven (or executed at run-time) to show that the initial condition is True.
Specification in SPARK 2014:
1package Stack_14
2 with SPARK_Mode,
3 Abstract_State => State,
4 Initializes => State,
5 Initial_Condition => Is_Empty -- Stating that Is_Empty holds
6 -- after initialization
7is
8 function Is_Empty return Boolean
9 with Global => State;
10
11 function Is_Full return Boolean
12 with Global => State;
13
14 function Top return Integer
15 with Global => State,
16 Pre => not Is_Empty;
17
18 procedure Push (X: in Integer)
19 with Global => (In_Out => State),
20 Pre => not Is_Full,
21 Post => Top = X;
22
23 procedure Pop (X: out Integer)
24 with Global => (In_Out => State),
25 Pre => not Is_Empty;
26end Stack_14;
Body in SPARK 2014:
1package body Stack_14
2 with SPARK_Mode,
3 Refined_State => (State => (S,
4 Pointer)) -- State refinement
5is
6 Max_Stack_Size : constant := 1024;
7 type Pointer_Range is range 0 .. Max_Stack_Size;
8 subtype Index_Range is Pointer_Range range 1 .. Max_Stack_Size;
9 type Vector is array (Index_Range) of Integer;
10
11 -- Declaration of constituents
12 S : Vector;
13 Pointer : Pointer_Range;
14
15 -- The subprogram contracts are refined in terms of the constituents.
16 -- Expression functions could be used where applicable
17
18 function Is_Empty return Boolean is (Pointer = 0)
19 with Refined_Global => Pointer;
20
21 function Is_Full return Boolean is (Pointer = Max_Stack_Size)
22 with Refined_Global => Pointer;
23
24 function Top return Integer is (S (Pointer))
25 with Refined_Global => (Pointer, S);
26
27 procedure Push(X: in Integer)
28 with Refined_Global => (In_Out => (Pointer, S))
29 is
30 begin
31 Pointer := Pointer + 1;
32 S (Pointer) := X;
33 end Push;
34
35 procedure Pop(X: out Integer)
36 with Refined_Global => (Input => S,
37 In_Out => Pointer)
38 is
39 begin
40 X := S (Pointer);
41 Pointer := Pointer - 1;
42 end Pop;
43begin
44 -- Initialization - we promised to initialize the state
45 -- and that initially the stack will be empty
46 Pointer := 0; -- Is_Empty is True.
47 S := Vector'(Index_Range => 0);
48end Stack_14;
Private, abstract state, refining onto state of private child
The following example shows a parent package Power that contains an own variable (a state abstraction). This state abstraction is refined onto state abstractions of two private children Source_A and Source_B.
Specification of Parent in SPARK 2005:
1-- Use of child packages to encapsulate state
2package Power_05
3--# own State;
4--# initializes State;
5is
6 procedure Read_Power(Level : out Integer);
7 --# global State;
8 --# derives Level from State;
9end Power_05;
Body of Parent in SPARK 2005:
1with Power_05.Source_A_05, Power_05.Source_B_05;
2
3package body Power_05
4--# own State is Power_05.Source_A_05.State,
5--# Power_05.Source_B_05.State;
6is
7
8 procedure Read_Power(Level : out Integer)
9 --# global Source_A_05.State, Source_B_05.State;
10 --# derives
11 --# Level
12 --# from
13 --# Source_A_05.State,
14 --# Source_B_05.State;
15 is
16 Level_A : Integer;
17 Level_B : Integer;
18 begin
19 Source_A_05.Read (Level_A);
20 Source_B_05.Read (Level_B);
21 Level := Level_A + Level_B;
22 end Read_Power;
23
24end Power_05;
Specifications of Private Children in SPARK 2005:
1--# inherit Power_05;
2private package Power_05.Source_A_05
3--# own State;
4--# initializes State;
5is
6 procedure Read (Level : out Integer);
7 --# global State;
8 --# derives Level from State;
9end Power_05.Source_A_05;
1--# inherit Power_05;
2private package Power_05.Source_B_05
3--# own State;
4--# initializes State;
5is
6 procedure Read (Level : out Integer);
7 --# global State;
8 --# derives Level from State;
9end Power_05.Source_B_05;
Bodies of Private Children in SPARK 2005:
1package body Power_05.Source_A_05
2--# own State is S;
3is
4 S : Integer := 0;
5
6 procedure Read (Level : out Integer)
7 --# global in S;
8 --# derives Level from S;
9 is
10 begin
11 Level := S;
12 end Read;
13end Power_05.Source_A_05;
1package body Power_05.Source_B_05
2--# own State is S;
3is
4 S : Integer := 0;
5
6 procedure Read (Level : out Integer)
7 --# global in S;
8 --# derives Level from S;
9 is
10 begin
11 Level := S;
12 end Read;
13end Power_05.Source_B_05;
Specification of Parent in SPARK 2014:
1-- Use of child packages to encapsulate state
2package Power_14
3 with SPARK_Mode,
4 Abstract_State => State,
5 Initializes => State
6is
7 procedure Read_Power(Level : out Integer)
8 with Global => State,
9 Depends => (Level => State);
10end Power_14;
Body of Parent in SPARK 2014:
1with Power_14.Source_A_14,
2 Power_14.Source_B_14;
3
4package body Power_14
5 with SPARK_Mode,
6 Refined_State => (State => (Power_14.Source_A_14.State,
7 Power_14.Source_B_14.State))
8is
9 procedure Read_Power(Level : out Integer)
10 with Refined_Global => (Source_A_14.State, Source_B_14.State),
11 Refined_Depends => (Level => (Source_A_14.State,
12 Source_B_14.State))
13 is
14 Level_A : Integer;
15 Level_B : Integer;
16 begin
17 Source_A_14.Read (Level_A);
18 Source_B_14.Read (Level_B);
19 Level := Level_A + Level_B;
20 end Read_Power;
21end Power_14;
Specifications of Private Children in SPARK 2014:
1private package Power_14.Source_A_14
2 with SPARK_Mode,
3 Abstract_State => (State with Part_Of =>Power_14.State),
4 Initializes => State
5is
6 procedure Read (Level : out Integer)
7 with Global => State,
8 Depends => (Level => State);
9end Power_14.Source_A_14;
1private package Power_14.Source_B_14
2 with SPARK_Mode,
3 Abstract_State => (State with Part_Of => Power_14.State),
4 Initializes => State
5is
6 procedure Read (Level : out Integer)
7 with Global => State,
8 Depends => (Level => State);
9end Power_14.Source_B_14;
Bodies of Private Children in SPARK 2014:
1package body Power_14.Source_A_14
2 with SPARK_Mode,
3 Refined_State => (State => S)
4is
5 S : Integer := 0;
6
7 procedure Read (Level : out Integer)
8 with Refined_Global => (Input => S),
9 Refined_Depends => (Level => S)
10 is
11 begin
12 Level := S;
13 end Read;
14end Power_14.Source_A_14;
1package body Power_14.Source_B_14
2 with SPARK_Mode,
3 Refined_State => (State => S)
4is
5 S : Integer := 0;
6
7 procedure Read (Level : out Integer)
8 with Refined_Global => (Input => S),
9 Refined_Depends => (Level => S)
10 is
11 begin
12 Level := S;
13 end Read;
14end Power_14.Source_B_14;
Private, abstract state, refining onto concrete state of embedded package
This example is based around the packages from section Private, abstract state, refining onto concrete state of embedded package, with the private child packages converted into embedded packages and the refinement onto concrete visible state.
Specification in SPARK 2005:
1-- Use of embedded packages to encapsulate state
2package Power_05
3--# own State;
4is
5 procedure Read_Power(Level : out Integer);
6 --# global State;
7 --# derives Level from State;
8end Power_05;
Body in SPARK 2005:
1package body Power_05
2--# own State is Source_A.State,
3--# Source_B.State;
4is
5
6 -- Embedded package spec for Source_A
7 package Source_A
8 --# own State;
9 is
10 procedure Read (Level : out Integer);
11 --# global State;
12 --# derives Level from State;
13 end Source_A;
14
15 -- Embedded package spec for Source_B.
16 package Source_B
17 --# own State;
18 is
19 procedure Read (Level : out Integer);
20 --# global State;
21 --# derives Level from State;
22 end Source_B;
23
24 -- Embedded package body for Source_A
25 package body Source_A
26 is
27 State : Integer;
28
29 procedure Read (Level : out Integer)
30 is
31 begin
32 Level := State;
33 end Read;
34 end Source_A;
35
36 -- Embedded package body for Source_B
37 package body Source_B
38 is
39 State : Integer;
40
41 procedure Read (Level : out Integer)
42 is
43 begin
44 Level := State;
45 end Read;
46
47 end Source_B;
48
49 procedure Read_Power(Level : out Integer)
50 --# global Source_A.State, Source_B.State;
51 --# derives
52 --# Level
53 --# from
54 --# Source_A.State,
55 --# Source_B.State;
56 is
57 Level_A : Integer;
58 Level_B : Integer;
59 begin
60 Source_A. Read (Level_A);
61 Source_B.Read (Level_B);
62 Level := Level_A + Level_B;
63 end Read_Power;
64
65end Power_05;
Specification in SPARK 2014:
1-- Use of embedded packages to encapsulate state
2package Power_14
3 with SPARK_Mode,
4 Abstract_State => State,
5 Initializes => State
6is
7 procedure Read_Power(Level : out Integer)
8 with Global => State,
9 Depends => (Level => State);
10end Power_14;
Body in SPARK 2014:
1package body Power_14
2 with SPARK_Mode,
3 Refined_State => (State => (Source_A.State,
4 Source_B.State))
5is
6 -- Embedded package spec for Source_A
7 package Source_A
8 with Initializes => State
9 is
10 State : Integer := 0;
11
12 procedure Read (Level : out Integer)
13 with Global => State,
14 Depends => (Level => State);
15 end Source_A;
16
17 -- Embedded package spec for Source_B.
18 package Source_B
19 with Initializes => State
20 is
21 State : Integer := 0;
22
23 procedure Read (Level : out Integer)
24 with Global => State,
25 Depends => (Level => State);
26 end Source_B;
27
28 -- Embedded package body for Source_A
29 package body Source_A is
30 procedure Read (Level : out Integer) is
31 begin
32 Level := State;
33 end Read;
34 end Source_A;
35
36 -- Embedded package body for Source_B
37 package body Source_B is
38 procedure Read (Level : out Integer) is
39 begin
40 Level := State;
41 end Read;
42 end Source_B;
43
44 procedure Read_Power(Level : out Integer)
45 with Refined_Global => (Source_A.State,
46 Source_B.State),
47 Refined_Depends => (Level => (Source_A.State,
48 Source_B.State))
49 is
50 Level_A : Integer;
51 Level_B : Integer;
52 begin
53 Source_A. Read (Level_A);
54 Source_B.Read (Level_B);
55 Level := Level_A + Level_B;
56 end Read_Power;
57end Power_14;
Private, abstract state, refining onto mixture of the above
This example is based around the packages from sections Private, abstract state, refining onto state of private child and Private, abstract state, refining onto concrete state of embedded package. Source_A is an embedded package, while Source_B is a private child. In order to avoid repetition, the code of this example is not being presented.
External Variables
Basic Input and Output Device Drivers
The following example shows a main program - Copy - that reads all available data from a given input port, stores it internally during the reading process in a stack and then outputs all the data read to an output port. The specifications of the stack packages are not presented since they are identical to previous examples.
Specification of main program in SPARK 2005:
1with Input_Port_05, Output_Port_05, Stacks_05;
2--# inherit Input_Port_05, Output_Port_05, Stacks_05;
3--# main_program;
4procedure Copy_05
5--# global in Input_Port_05.Input_State;
6--# out Output_Port_05.Output_State;
7--# derives Output_Port_05.Output_State from Input_Port_05.Input_State;
8is
9 The_Stack : Stacks_05.Stack;
10 Value : Integer;
11 Done : Boolean;
12 Final_Value : constant Integer := 999;
13begin
14 Stacks_05.Clear(The_Stack);
15 loop
16 Input_Port_05.Read_From_Port(Value);
17 Stacks_05.Push(The_Stack, Value);
18 Done := Value = Final_Value;
19 exit when Done;
20 end loop;
21 loop
22 Stacks_05.Pop(The_Stack, Value);
23 Output_Port_05.Write_To_Port(Value);
24 exit when Stacks_05.Is_Empty(The_Stack);
25 end loop;
26end Copy_05;
Specification of input port in SPARK 2005:
1package Input_Port_05
2 --# own in Input_State;
3is
4 procedure Read_From_Port(Input_Value : out Integer);
5 --# global in Input_State;
6 --# derives Input_Value from Input_State;
7
8end Input_Port_05;
Body of input port in SPARK 2005:
1package body Input_Port_05
2is
3
4 Input_State : Integer;
5 for Input_State'Address use
6 System.Storage_Elements.To_Address (16#ACECAE0#);
7 pragma Volatile (Input_State);
8
9 procedure Read_From_Port(Input_Value : out Integer)
10 is
11 begin
12 Input_Value := Input_State;
13 end Read_From_Port;
14
15end Input_Port_05;
Specification of output port in SPARK 2005:
1package Output_Port_05
2 --# own out Output_State;
3is
4 procedure Write_To_Port(Output_Value : in Integer);
5 --# global out Output_State;
6 --# derives Output_State from Output_Value;
7end Output_Port_05;
Body of output port in SPARK 2005:
1package body Output_Port_05
2is
3
4 Output_State : Integer;
5 for Output_State'Address use
6 System.Storage_Elements.To_Address (16#ACECAF0#);
7 pragma Volatile (Output_State);
8
9 procedure Write_To_Port(Output_Value : in Integer)
10 is
11 begin
12 Output_State := Output_Value;
13 end Write_To_Port;
14
15end Output_Port_05;
Specification of main program in SPARK 2014:
1with Input_Port_14,
2 Output_Port_14,
3 Stacks_14;
4-- No need to specify that Copy_14 is a main program
5
6procedure Copy_14
7 with SPARK_Mode,
8 Global => (Input => Input_Port_14.Input_State,
9 Output => Output_Port_14.Output_State),
10 Depends => (Output_Port_14.Output_State => Input_Port_14.Input_State)
11is
12 The_Stack : Stacks_14.Stack;
13 Value : Integer;
14 Done : Boolean;
15 Final_Value : constant Integer := 999;
16begin
17 Stacks_14.Clear(The_Stack);
18 loop
19 Input_Port_14.Read_From_Port(Value);
20 Stacks_14.Push(The_Stack, Value);
21 Done := Value = Final_Value;
22 exit when Done;
23 end loop;
24 loop
25 Stacks_14.Pop(The_Stack, Value);
26 Output_Port_14.Write_To_Port(Value);
27 exit when Stacks_14.Is_Empty(The_Stack);
28 end loop;
29end Copy_14;
Specification of input port in SPARK 2014:
1package Input_Port_14
2 with SPARK_Mode,
3 Abstract_State => (Input_State with External => Async_Writers)
4is
5 procedure Read_From_Port(Input_Value : out Integer)
6 with Global => (Input => Input_State),
7 Depends => (Input_Value => Input_State);
8end Input_Port_14;
Specification of output port in SPARK 2014:
1package Output_Port_14
2 with SPARK_Mode,
3 Abstract_State => (Output_State with External => Async_Readers)
4is
5 procedure Write_To_Port(Output_Value : in Integer)
6 with Global => (Output => Output_State),
7 Depends => (Output_State => Output_Value);
8end Output_Port_14;
Body of input port in SPARK 2014:
This is as per SPARK 2005, but uses aspects instead of representation clauses and pragmas.
1with System.Storage_Elements;
2
3package body Input_Port_14
4 with SPARK_Mode,
5 Refined_State => (Input_State => Input_S)
6is
7 Input_S : Integer
8 with Volatile,
9 Async_Writers,
10 Address => System.Storage_Elements.To_Address (16#ACECAE0#);
11
12 procedure Read_From_Port(Input_Value : out Integer)
13 with Refined_Global => (Input => Input_S),
14 Refined_Depends => (Input_Value => Input_S)
15 is
16 begin
17 Input_Value := Input_S;
18 end Read_From_Port;
19end Input_Port_14;
Body of output port in SPARK 2014:
This is as per SPARK 2005, but uses aspects instead of representation clauses and pragmas.
1with System.Storage_Elements;
2
3package body Output_Port_14
4 with SPARK_Mode,
5 Refined_State => (Output_State => Output_S)
6is
7 Output_S : Integer
8 with Volatile,
9 Async_Readers,
10 Address => System.Storage_Elements.To_Address (16#ACECAF0#);
11
12 procedure Write_To_Port(Output_Value : in Integer)
13 with Refined_Global => (Output => Output_S),
14 Refined_Depends => (Output_S => Output_Value)
15 is
16 begin
17 Output_S := Output_Value;
18 end Write_To_Port;
19end Output_Port_14;
Input driver using 'Tail in a contract
This example uses the Input_Port package from section Basic Input and Output Device Drivers and adds a contract using the ‘Tail attribute. The example also use the Always_Valid attribute in order to allow proof to succeed (otherwise, there is no guarantee in the proof context that the value read from the port is of the correct type).
SPARK 2014 does not have the attribute ‘Tail but, often, an equivalent proof can be achieved using assert pragmas. Neither is there a direct equivalent of the Always_Valid attribute but the paragma Assume may be used to the same effect.
Specification in SPARK 2005:
1package Input_Port
2 --# own in Inputs : Integer;
3is
4 procedure Read_From_Port(Input_Value : out Integer);
5 --# global in Inputs;
6 --# derives Input_Value from Inputs;
7 --# post (Inputs~ = 0 -> (Input_Value = Inputs'Tail (Inputs~))) and
8 --# (Inputs~ /= 0 -> (Input_Value = Inputs~));
9
10end Input_Port;
Body in SPARK 2005:
1package body Input_Port
2is
3
4 Inputs : Integer;
5 for Inputs'Address use
6 System.Storage_Elements.To_Address (16#ACECAF0#);
7
8 --# assert Inputs'Always_Valid;
9 pragma Volatile (Inputs);
10
11 procedure Read_From_Port(Input_Value : out Integer)
12 is
13 begin
14 Input_Value := Inputs;
15 if Input_Value = 0 then
16 Input_Value := Inputs;
17 end if;
18 end Read_From_Port;
19
20end Input_Port;
Specification in SPARK 2014:
1package Input_Port_14
2 with SPARK_Mode,
3 Abstract_State => (Inputs with External => Async_Writers)
4is
5 procedure Read_From_Port(Input_Value : out Integer)
6 with Global => Inputs,
7 Depends => (Input_Value => Inputs);
8end Input_Port_14;
Body in SPARK 2014:
1with System.Storage_Elements;
2
3package body Input_Port_14
4 with SPARK_Mode,
5 Refined_State => (Inputs => Input_Port)
6is
7 Input_Port : Integer
8 with Volatile,
9 Async_Writers,
10 Address => System.Storage_Elements.To_Address (16#ACECAF0#);
11
12 procedure Read_From_Port(Input_Value : out Integer)
13 with Refined_Global => Input_Port,
14 Refined_Depends => (Input_Value => Input_Port)
15 is
16 First_Read : Integer;
17 Second_Read : Integer;
18 begin
19 Second_Read := Input_Port; -- Ensure Second_Read is initialized
20 pragma Assume (Second_Read'Valid);
21 First_Read := Second_Read; -- but it is infact the First_Read.
22 if First_Read = 0 then
23 Second_Read := Input_Port; -- Now it is the Second_Read
24 pragma Assume (Second_Read'Valid);
25 Input_Value := Second_Read;
26 else
27 Input_Value := First_Read;
28 end if;
29 pragma Assert ((First_Read = 0 and then Input_Value = Second_Read)
30 or else (Input_Value = First_Read));
31 end Read_From_Port;
32end Input_Port_14;
Output driver using 'Append in a contract
This example uses the Output package from section Basic Input and Output Device Drivers and adds a contract using the ‘Append attribute.
SPARK 2014 does not have the attribute ‘Append but, often, an equivalent proof can be achieved using assert pragmas.
Specification in SPARK 2005:
1package Output_Port
2 --# own out Outputs : Integer;
3is
4 procedure Write_To_Port(Output_Value : in Integer);
5 --# global out Outputs;
6 --# derives Outputs from Output_Value;
7 --# post ((Output_Value = -1) ->
8 --# (Outputs =
9 --# Outputs'Append (Outputs'Append (Outputs~, 0), Output_Value)))
10 --# and
11 --# ((Output_Value /= -1) ->
12 --# (Outputs =
13 --# Outputs'Append (Outputs~, Output_Value)));
14end Output_Port;
Body in SPARK 2005:
1package body Output_Port
2is
3
4 Outputs : Integer;
5 for Outputs'Address use System.Storage_Elements.To_Address (16#ACECAF10#);
6 pragma Volatile (Outputs);
7
8 procedure Write_To_Port(Output_Value : in Integer)
9 is
10 begin
11 if Output_Value = -1 then
12 Outputs := 0;
13 end if;
14
15 Outputs := Output_Value;
16 end Write_To_Port;
17
18end Output_Port;
Specification in SPARK 2014:
1package Output_Port_14
2 with SPARK_Mode,
3 Abstract_State => (Outputs with External => Async_Readers)
4is
5 procedure Write_To_Port(Output_Value : in Integer)
6 with Global => (Output => Outputs),
7 Depends => (Outputs => Output_Value);
8end Output_Port_14;
Body in SPARK 2014:
1with System.Storage_Elements;
2
3package body Output_Port_14
4 with SPARK_Mode,
5 Refined_State => (Outputs => Output_Port)
6is
7 Output_Port : Integer
8 with Volatile,
9 Async_Readers,
10 Address => System.Storage_Elements.To_Address (16#ACECAF10#);
11
12 -- This is a simple subprogram that always updates the Output_Shadow with
13 -- the single value which is written to the output port.
14 procedure Write_It (Output_Value : in Integer; Output_Shadow : out Integer)
15 with Global => (Output => Output_Port),
16 Depends => ((Output_Port, Output_Shadow) => Output_Value),
17 Post => Output_Shadow = Output_Value
18 is
19 begin
20 Output_Shadow := Output_Value;
21 Output_Port := Output_Shadow;
22 end Write_It;
23
24
25 procedure Write_To_Port(Output_Value : in Integer)
26 with Refined_Global => (Output => Output_Port),
27 Refined_Depends => (Output_Port => Output_Value)
28 is
29 Out_1, Out_2 : Integer;
30 begin
31 if Output_Value = -1 then
32 Write_It (0, Out_1);
33 Write_It (Output_Value, Out_2);
34 else
35 Write_It (Output_Value, Out_1);
36 Out_2 := Out_1; -- Avoids flow error.
37 end if;
38
39 pragma Assert (if Output_Value = -1 then
40 Out_1 = 0 and Out_2 = Output_Value
41 else
42 Out_1 = Output_Value);
43 end Write_To_Port;
44end Output_Port_14;
Refinement of external state - voting input switch
The following example presents an abstract view of the reading of 3 individual switches and the voting performed on the values read.
Abstract Switch specification in SPARK 2005:
1package Switch
2--# own in State;
3is
4
5 type Reading is (on, off, unknown);
6
7 function ReadValue return Reading;
8 --# global in State;
9
10end Switch;
Component Switch specifications in SPARK 2005:
1--# inherit Switch;
2private package Switch.Val1
3--# own in State;
4is
5 function Read return Switch.Reading;
6 --# global in State;
7
8end Switch.Val1;
1--# inherit Switch;
2private package Switch.Val2
3--# own in State;
4is
5 function Read return Switch.Reading;
6 --# global in State;
7
8end Switch.Val2;
1--# inherit Switch;
2private package Switch.Val3
3--# own in State;
4is
5 function Read return Switch.Reading;
6 --# global in State;
7
8end Switch.Val3;
Switch body in SPARK 2005:
1with Switch.Val1;
2with Switch.Val2;
3with Switch.Val3;
4package body Switch
5--# own State is in Switch.Val1.State,
6--# in Switch.Val2.State,
7--# in Switch.Val3.State;
8is
9
10 subtype Value is Integer range -1 .. 1;
11 subtype Score is Integer range -3 .. 3;
12 type ConvertToValueArray is array (Reading) of Value;
13 type ConvertToReadingArray is array (Score) of Reading;
14
15 ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(on => 1,
16 unknown => 0,
17 off => -1);
18 ConvertToReading : constant ConvertToReadingArray :=
19 ConvertToReadingArray'(-3 .. -2 => off,
20 -1 .. 1 => unknown,
21 2 ..3 => on);
22
23 function ReadValue return Reading
24 --# global in Val1.State;
25 --# in Val2.State;
26 --# in Val3.State;
27 is
28 A, B, C : Reading;
29 begin
30 A := Val1.Read;
31 B := Val2.Read;
32 C := Val3.Read;
33 return ConvertToReading (ConvertToValue (A) +
34 ConvertToValue (B) + ConvertToValue (C));
35 end ReadValue;
36
37end Switch;
Abstract Switch specification in SPARK 2014:
1package Switch
2 with SPARK_Mode,
3 Abstract_State => (State with External => Async_Writers)
4is
5 type Reading is (on, off, unknown);
6
7 function ReadValue return Reading
8 with Volatile_Function,
9 Global => (Input => State);
10end Switch;
Component Switch specifications in SPARK 2014:
1private package Switch.Val1
2 with SPARK_Mode,
3 Abstract_State => (State with External => Async_Writers,
4 Part_Of => Switch.State)
5is
6 function Read return Switch.Reading
7 with Volatile_Function,
8 Global => (Input => State);
9end Switch.Val1;
1private package Switch.Val2
2 with SPARK_Mode,
3 Abstract_State => (State with External => Async_Writers,
4 Part_Of => Switch.State)
5is
6 function Read return Switch.Reading
7 with Volatile_Function,
8 Global => (Input => State);
9end Switch.Val2;
1private package Switch.Val3
2 with SPARK_Mode,
3 Abstract_State => (State with External => Async_Writers,
4 Part_Of => Switch.State)
5is
6 function Read return Switch.Reading
7 with Volatile_Function,
8 Global => (Input => State);
9end Switch.Val3;
Switch body in SPARK 2014:
1with Switch.Val1,
2 Switch.Val2,
3 Switch.Val3;
4
5package body Switch
6 -- State is refined onto three states, each of which has properties
7 -- Volatile and Input
8 with SPARK_Mode,
9 Refined_State => (State => (Switch.Val1.State,
10 Switch.Val2.State,
11 Switch.Val3.State))
12is
13 subtype Value is Integer range -1 .. 1;
14 subtype Score is Integer range -3 .. 3;
15 type ConvertToValueArray is array (Reading) of Value;
16 type ConvertToReadingArray is array (Score) of Reading;
17
18 ConvertToValue : constant ConvertToValueArray :=
19 ConvertToValueArray'(on => 1,
20 unknown => 0,
21 off => -1);
22 ConvertToReading : constant ConvertToReadingArray :=
23 ConvertToReadingArray'(-3 .. -2 => off,
24 -1 .. 1 => unknown,
25 2 .. 3 => on);
26
27 function ReadValue return Reading
28 with Refined_Global => (Input => (Val1.State, Val2.State, Val3.State))
29 is
30 A, B, C : Reading;
31 begin
32 A := Val1.Read;
33 B := Val2.Read;
34 C := Val3.Read;
35 return ConvertToReading (ConvertToValue (A) +
36 ConvertToValue (B) + ConvertToValue (C));
37 end ReadValue;
38end Switch;
Complex I/O Device
The following example illustrates a more complex I/O device: the device is fundamentally an output device but an acknowledgement has to be read from it. In addition, a local register stores the last value written to avoid writes that would just re-send the same value. The own variable is then refined into a normal variable, an input external variable and an output external variable.
Specification in SPARK 2005:
1package Device
2--# own State;
3--# initializes State;
4is
5 procedure Write (X : in Integer);
6 --# global in out State;
7 --# derives State from State, X;
8end Device;
Body in SPARK 2005:
1package body Device
2--# own State is OldX,
3--# in StatusPort,
4--# out Register;
5-- refinement on to mix of external and ordinary variables
6is
7 type Status_Port_Type is mod 2**32;
8
9 OldX : Integer := 0; -- only component that needs initialization
10 StatusPort : Status_Port_Type;
11 pragma Volatile (StatusPort);
12 -- address clause would be added here
13
14 Register : Integer;
15 pragma Volatile (Register);
16 -- address clause would be added here
17
18 procedure WriteReg (X : in Integer)
19 --# global out Register;
20 --# derives Register from X;
21 is
22 begin
23 Register := X;
24 end WriteReg;
25
26 procedure ReadAck (OK : out Boolean)
27 --# global in StatusPort;
28 --# derives OK from StatusPort;
29 is
30 RawValue : Status_Port_Type;
31 begin
32 RawValue := StatusPort; -- only assignment allowed here
33 OK := RawValue = 16#FFFF_FFFF#;
34 end ReadAck;
35
36 procedure Write (X : in Integer)
37 --# global in out OldX;
38 --# out Register;
39 --# in StatusPort;
40 --# derives OldX,Register from OldX, X &
41 --# null from StatusPort;
42 is
43 OK : Boolean;
44 begin
45 if X /= OldX then
46 OldX := X;
47 WriteReg (X);
48 loop
49 ReadAck (OK);
50 exit when OK;
51 end loop;
52 end if;
53 end Write;
54end Device;
Specification in SPARK 2014:
1package Device
2 with SPARK_Mode,
3 Abstract_State => (State with External => (Async_Readers,
4 Async_Writers)),
5 Initializes => State
6is
7 procedure Write (X : in Integer)
8 with Global => (In_Out => State),
9 Depends => (State =>+ X);
10end Device;
Body in SPARK 2014:
1package body Device
2 with SPARK_Mode,
3 Refined_State => (State => (OldX,
4 StatusPort,
5 Register))
6 -- refinement on to mix of external and ordinary variables
7is
8 type Status_Port_Type is mod 2**32;
9
10 OldX : Integer := 0; -- only component that needs initialization
11
12 StatusPort : Status_Port_Type
13 with Volatile,
14 Async_Writers;
15 -- address clause would be added here
16
17 Register : Integer
18 with Volatile,
19 Async_Readers;
20 -- address clause would be added here
21
22 procedure WriteReg (X : in Integer)
23 with Global => (Output => Register),
24 Depends => (Register => X)
25 is
26 begin
27 Register := X;
28 end WriteReg;
29
30 procedure ReadAck (OK : out Boolean)
31 with Global => (Input => StatusPort),
32 Depends => (OK => StatusPort)
33 is
34 RawValue : Status_Port_Type;
35 begin
36 RawValue := StatusPort; -- only assignment allowed here
37 OK := RawValue = 16#FFFF_FFFF#;
38 end ReadAck;
39
40 procedure Write (X : in Integer)
41 with Refined_Global => (Input => StatusPort,
42 Output => Register,
43 In_Out => OldX),
44 Refined_Depends => ((OldX,
45 Register) => (OldX,
46 X),
47 null => StatusPort)
48 is
49 OK : Boolean;
50 begin
51 if X /= OldX then
52 OldX := X;
53 WriteReg (X);
54 loop
55 ReadAck (OK);
56 exit when OK;
57 end loop;
58 end if;
59 end Write;
60end Device;
Increasing values in input stream
The following example illustrates an input port from which values are read. According to its postcondition, procedure Increases checks whether the first values read from the sequence are in ascending order. This example shows that postconditions can refer to multiple individual elements of the input stream.
In SPARK 2014 we can use assert pragmas in the subprogram instead of specifying the action in the postcondition, as was done in Input driver using 'Tail in a contract. Another alternative, as shown in this example, is to use a formal parameter of a private type to keep a trace of the values read.
Specification in SPARK 2005:
1 package Inc
2--# own in Sensor : Integer;
3is
4 procedure Increases (Result : out Boolean;
5 Valid : out Boolean);
6 --# global in Sensor;
7 --# post Valid -> (Result <-> Sensor'Tail (Sensor~) > Sensor~);
8
9end Inc;
Body in SPARK 2005:
1with System.Storage_Elements;
2package body Inc
3-- Cannot refine own variable Sensor as it has been given a concrete type.
4is
5 Sensor : Integer;
6 for Sensor'Address use System.Storage_Elements.To_Address (16#DEADBEE0#);
7 pragma Volatile (Sensor);
8
9 procedure Read (V : out Integer;
10 Valid : out Boolean)
11 --# global in Sensor;
12 --# post (Valid -> V = Sensor~) and
13 --# (Sensor = Sensor'Tail (Sensor~));
14 is
15 Tmp : Integer;
16 begin
17 Tmp := Sensor;
18 if Tmp'Valid then
19 V := Tmp;
20 Valid := True;
21 --# check Sensor = Sensor'Tail (Sensor~);
22 else
23 V := 0;
24 Valid := False;
25 end if;
26 end Read;
27
28 procedure Increases (Result : out Boolean;
29 Valid : out Boolean)
30 is
31 A, B : Integer;
32 begin
33 Result := False;
34 Read (A, Valid);
35 if Valid then
36 Read (B, Valid);
37 if Valid then
38 Result := B > A;
39 end if;
40 end if;
41 end Increases;
42
43end Inc;
Specification in SPARK 2014:
1package Inc
2 with SPARK_Mode,
3 Abstract_State => (Sensor with External => Async_Writers)
4is
5 -- Declare a private type which will keep a trace of the
6 -- values read.
7 type Increasing_Indicator is private;
8
9 -- Access (ghost) functions for the private type only intended for
10 -- use in pre and post conditions or other assertion expressions
11 function First (Indicator : Increasing_Indicator) return Integer
12 with Ghost;
13
14 function Second (Indicator : Increasing_Indicator) return Integer
15 with Ghost;
16
17 -- Used to check that the value returned by procedure Increases
18 -- is valid (Invalid values have not been read from the Sensor).
19 function Is_Valid (Indicator : Increasing_Indicator) return Boolean;
20
21 -- Use this function to determine whether the result of the procedure
22 -- Increases indicates an increasing value.
23 -- It can only be called if Is_Valid (Indicator)
24 function Is_Increasing (Indicator : Increasing_Indicator) return Boolean
25 with Pre => Is_Valid (Indicator);
26
27 procedure Increases (Result : out Increasing_Indicator)
28 with Global => Sensor,
29 Post => (if Is_Valid (Result) then Is_Increasing (Result)=
30 (Second (Result) > First (Result)));
31
32private
33 type Increasing_Indicator is record
34 Valid : Boolean;
35 First, Second : Integer;
36 end record;
37end Inc;
Body in SPARK 2014:
1with System.Storage_Elements;
2
3package body Inc
4 with SPARK_Mode,
5 Refined_State => (Sensor => S)
6is
7 pragma Warnings (Off);
8 S : Integer
9 with Volatile,
10 Async_Writers,
11 Address => System.Storage_Elements.To_Address (16#DEADBEE0#);
12 pragma Warnings (On);
13
14 function First (Indicator : Increasing_Indicator) return Integer is
15 (Indicator.First);
16
17 function Second (Indicator : Increasing_Indicator) return Integer is
18 (Indicator.Second);
19
20 function Is_Valid (Indicator : Increasing_Indicator) return Boolean is
21 (Indicator.Valid);
22
23 function Is_Increasing (Indicator : Increasing_Indicator) return Boolean is
24 (Indicator.Second > Indicator.First);
25
26 pragma Warnings (Off);
27 procedure Read (V : out Integer;
28 Valid : out Boolean)
29 with Global => S,
30 Post => (if Valid then V'Valid)
31 is
32 Tmp : Integer;
33 begin
34 pragma Warnings (On);
35 Tmp := S;
36 pragma Warnings (Off);
37 if Tmp'Valid then
38 pragma Warnings (On);
39 V := Tmp;
40 Valid := True;
41 else
42 V := 0;
43 Valid := False;
44 end if;
45 end Read;
46
47 procedure Increases (Result : out Increasing_Indicator)
48 with Refined_Global => S
49 is
50 begin
51 Read (Result.First, Result.Valid);
52 if Result.Valid then
53 Read (Result.Second, Result.Valid);
54 else
55 Result.Second := 0;
56 end if;
57 end Increases;
58end Inc;
Package Inheritance
SPARK 2014 does not have the SPARK 2005 concept of package inheritance. It has the same package visibility rules as Ada.
Contracts with remote state
The following example illustrates indirect access to the state of one package by another via an intermediary. Raw_Data stores some data, which has preprocessing performed on it by Processing and on which Calculate performs some further processing (although the corresponding bodies are not given, Read_Calculated_Value in Calculate calls through to Read_Processed_Data in Processing, which calls through to Read in Raw_Data).
Specifications in SPARK 2005:
1package Raw_Data
2--# own State;
3--# Initializes State;
4is
5
6 function Data_Is_Valid return Boolean;
7 --# global State;
8
9 function Get_Value return Integer;
10 --# global State;
11
12 procedure Read_Next;
13 --# global in out State;
14 --# derives State from State;
15
16
17end Raw_Data;
1with Raw_Data;
2--# inherit Raw_Data;
3package Processing
4--# own State;
5--# Initializes State;
6is
7
8 procedure Get_Processed_Data (Value : out Integer);
9 --# global in Raw_Data.State;
10 --# in out State;
11 --# derives Value, State from State, Raw_Data.State;
12 --# pre Raw_Data.Data_Is_Valid (Raw_Data.State);
13
14end Processing;
1with Processing;
2--# inherit Processing, Raw_Data;
3package Calculate
4is
5
6 procedure Read_Calculated_Value (Value : out Integer);
7 --# global in out Processing.State;
8 --# in Raw_Data.State;
9 --# derives Value, Processing.State from Processing.State, Raw_Data.State;
10 --# pre Raw_Data.Data_Is_Valid (Raw_Data.State);
11
12end Calculate;
Specifications in SPARK 2014:
1package Raw_Data
2 with SPARK_Mode,
3 Abstract_State => (State with External => Async_Writers),
4 Initializes => State
5is
6 function Data_Is_Valid return Boolean
7 with Volatile_Function,
8 Global => State;
9
10 function Get_Value return Integer
11 with Volatile_Function,
12 Global => State;
13
14 procedure Read_Next
15 with Global => (In_Out => State),
16 Depends => (State => State);
17end Raw_Data;
1with Raw_Data;
2
3package Processing
4 with SPARK_Mode,
5 Abstract_State => State
6is
7 procedure Get_Processed_Data (Value : out Integer)
8 with Global => (Input => Raw_Data.State,
9 In_Out => State),
10 Depends => ((Value,
11 State) => (State,
12 Raw_Data.State)),
13 Pre => Raw_Data.Data_Is_Valid;
14end Processing;
1with Processing,
2 Raw_Data;
3
4package Calculate
5 with SPARK_Mode
6is
7 procedure Read_Calculated_Value (Value : out Integer)
8 with Global => (In_Out => Processing.State,
9 Input => Raw_Data.State),
10 Depends => ((Value,
11 Processing.State) => (Processing.State,
12 Raw_Data.State)),
13 Pre => Raw_Data.Data_Is_Valid;
14end Calculate;
Package nested inside package
See section Private, abstract state, refining onto concrete state of embedded package.
Package nested inside subprogram
This example is a modified version of that given in section Refinement of external state - voting input switch. It illustrates the use of a package nested within a subprogram.
Abstract Switch specification in SPARK 2005:
1package Switch
2--# own in State;
3is
4
5 type Reading is (on, off, unknown);
6
7 function ReadValue return Reading;
8 --# global in State;
9
10end Switch;
Component Switch specifications in SPARK 2005:
As in Refinement of external state - voting input switch
Switch body in SPARK 2005:
1with Switch.Val1;
2with Switch.Val2;
3with Switch.Val3;
4package body Switch
5--# own State is in Switch.Val1.State,
6--# in Switch.Val2.State,
7--# in Switch.Val3.State;
8is
9
10 subtype Value is Integer range -1 .. 1;
11 subtype Score is Integer range -3 .. 3;
12
13
14 function ReadValue return Reading
15 --# global in Val1.State;
16 --# in Val2.State;
17 --# in Val3.State;
18 is
19 A, B, C : Reading;
20
21 -- Embedded package to provide the capability to synthesize three inputs
22 -- into one.
23 --# inherit Switch;
24 package Conversion
25 is
26
27 function Convert_To_Reading
28 (Val_A : Switch.Reading;
29 Val_B : Switch.Reading;
30 Val_C : Switch.Reading) return Switch.Reading;
31
32 end Conversion;
33
34 package body Conversion
35 is
36
37 type ConvertToValueArray is array (Switch.Reading) of Switch.Value;
38 type ConvertToReadingArray is array (Switch.Score) of Switch.Reading;
39 ConvertToValue : constant ConvertToValueArray := ConvertToValueArray'(Switch.on => 1,
40 Switch.unknown => 0,
41 Switch.off => -1);
42
43 ConvertToReading : constant ConvertToReadingArray :=
44 ConvertToReadingArray'(-3 .. -2 => Switch.off,
45 -1 .. 1 => Switch.unknown,
46 2 ..3 => Switch.on);
47
48 function Convert_To_Reading
49 (Val_A : Switch.Reading;
50 Val_B : Switch.Reading;
51 Val_C : Switch.Reading) return Switch.Reading
52 is
53 begin
54
55 return ConvertToReading (ConvertToValue (Val_A) +
56 ConvertToValue (Val_B) + ConvertToValue (Val_C));
57 end Convert_To_Reading;
58
59 end Conversion;
60
61 begin
62 A := Val1.Read;
63 B := Val2.Read;
64 C := Val3.Read;
65 return Conversion.Convert_To_Reading
66 (Val_A => A,
67 Val_B => B,
68 Val_C => C);
69 end ReadValue;
70
71end Switch;
Abstract Switch specification in SPARK 2014:
1package Switch
2 with SPARK_Mode,
3 Abstract_State => (State with External => Async_Writers)
4is
5 type Reading is (on, off, unknown);
6
7 function ReadValue return Reading
8 with Volatile_Function,
9 Global => (Input => State);
10end Switch;
Component Switch specification in SPARK 2014:
As in Refinement of external state - voting input switch
Switch body in SPARK 2014:
1with Switch.Val1,
2 Switch.Val2,
3 Switch.Val3;
4
5package body Switch
6 -- State is refined onto three states, each of which has properties
7 -- Volatile and Input.
8 with SPARK_Mode,
9 Refined_State => (State => (Switch.Val1.State,
10 Switch.Val2.State,
11 Switch.Val3.State))
12is
13 subtype Value is Integer range -1 .. 1;
14 subtype Score is Integer range -3 .. 3;
15
16 function ReadValue return Reading
17 with Refined_Global => (Input => (Val1.State, Val2.State, Val3.State))
18 is
19 A, B, C : Reading;
20
21 -- Embedded package to provide the capability to synthesize three inputs
22 -- into one.
23 package Conversion is
24 function Convert_To_Reading
25 (Val_A : Switch.Reading;
26 Val_B : Switch.Reading;
27 Val_C : Switch.Reading) return Switch.Reading;
28 end Conversion;
29
30 package body Conversion is
31 type ConvertToValueArray is array (Switch.Reading) of Switch.Value;
32 type ConvertToReadingArray is array (Switch.Score) of Switch.Reading;
33 ConvertToValue : constant ConvertToValueArray :=
34 ConvertToValueArray'(Switch.on => 1,
35 Switch.unknown => 0,
36 Switch.off => -1);
37
38 ConvertToReading : constant ConvertToReadingArray :=
39 ConvertToReadingArray'(-3 .. -2 => Switch.off,
40 -1 .. 1 => Switch.unknown,
41 2 .. 3 => Switch.on);
42
43 function Convert_To_Reading
44 (Val_A : Switch.Reading;
45 Val_B : Switch.Reading;
46 Val_C : Switch.Reading) return Switch.Reading is
47 (ConvertToReading (ConvertToValue (Val_A) +
48 ConvertToValue (Val_B) +
49 ConvertToValue (Val_C)));
50 end Conversion;
51 begin -- begin statement of ReadValue function
52 A := Val1.Read;
53 B := Val2.Read;
54 C := Val3.Read;
55 return Conversion.Convert_To_Reading
56 (Val_A => A,
57 Val_B => B,
58 Val_C => C);
59 end ReadValue;
60end Switch;
Circular dependence and elaboration order
SPARK 2005 avoided issues of circular dependence and elaboration order dependencies through a combination of the inherit annotation and the restrictions that initialization expressions are constant, user defined subprograms cannot be called in the sequence of statements of a package body and a package can only initialize variables declared in its delarative part.
SPARK 2014 does not have the inherit annotation and only enforces the restriction that a package can only initialize an object declared in its declarative region. Hence, in SPARK 2014 two package bodies that depend on each other’s specification may be legal, as is calling a user defined subprogram.
Instead of the elaboration restrictions of SPARK 2005 a set of rules is applied in SPARK 2014 which determines when elaboration order control pragmas such as Elaborate_Body or Elaborate_All are required. These rules ensure the absence of elaboration order dependencies.
Examples of the features of SPARK 2014 elaboration order rules are given below. In the example described below the partial elaboration order would be either of P_14 or Q_14 specifications first followed by P_14 body because of the Elaborate_All on the specification of R_14 specification and the body of Q_14, then the elaboration of Q_14 body or the specification of R_14 and the body of R_14 after the elaboration of Q_14. Elaboration order dependencies are avoided by the (required) use of elaboration control pragmas.
Package Specifications in SPARK 2014:
1package P_14
2 with SPARK_Mode,
3 Abstract_State => P_State,
4 Initializes => (P_State, Global_Var),
5 Elaborate_Body
6is
7 Global_Var : Integer;
8
9 procedure Init (S : out Integer);
10end P_14;
1package Q_14
2 with SPARK_Mode,
3 Abstract_State => Q_State,
4 Initializes => Q_State
5is
6 type T is new Integer;
7
8 procedure Init (S : out T);
9end Q_14;
1with P_14;
2pragma Elaborate_All (P_14); -- Required because P_14.Global_Var
3 -- Is mentioned as input in the Initializes aspect
4package R_14
5 with SPARK_Mode,
6 Abstract_State => State,
7 Initializes => (State => P_14.Global_Var)
8is
9 procedure Op ( X : in Positive)
10 with Global => (In_Out => State);
11end R_14;
Package Bodies in SPARK 2014
1with Q_14;
2
3package body P_14
4 with SPARK_Mode,
5 Refined_State => (P_State => P_S)
6is
7 P_S : Q_14.T; -- The use of type Q.T does not require
8 -- the body of Q to be elaborated.
9
10 procedure Init (S : out Integer) is
11 begin
12 S := 5;
13 end Init;
14begin
15 -- Cannot call Q_14.Init here beacuse
16 -- this would require an Elaborate_All for Q_14
17 -- and would be detected as a circularity
18 Init (Global_Var);
19 P_S := Q_14.T (Global_Var);
20end P_14;
1with P_14;
2pragma Elaborate_All (P_14); -- Required because the elaboration of the
3 -- body of Q_14 (indirectly) calls P_14.Init
4package body Q_14
5 with SPARK_Mode,
6 Refined_State => (Q_State => Q_S)
7is
8 Q_S : T;
9
10 procedure Init (S : out T) is
11 V : Integer;
12 begin
13 P_14.Init (V);
14 if V > 0 and then V <= Integer'Last - 5 then
15 S := T(V + 5);
16 else
17 S := 5;
18 end if;
19 end Init;
20begin
21 Init (Q_S);
22end Q_14;
1with Q_14;
2pragma Elaborate_All (Q_14); -- Required because Q_14.Init is called
3 -- in the elaboration of the body of R_14
4use type Q_14.T;
5
6package body R_14
7 with SPARK_Mode,
8 Refined_State => (State => R_S)
9is
10 R_S : Q_14.T;
11 procedure Op ( X : in Positive)
12 with Refined_Global => (In_Out => R_S)
13 is
14 begin
15 if R_S <= Q_14.T'Last - Q_14.T (X) then
16 R_S := R_S + Q_14.T (X);
17 else
18 R_S := 0;
19 end if;
20 end Op;
21begin
22 Q_14.Init (R_S);
23 if P_14.Global_Var > 0
24 and then R_S <= Q_14.T'Last - Q_14.T (P_14.Global_Var)
25 then
26 R_S := R_S + Q_14.T (P_14.Global_Var);
27 else
28 R_S := Q_14.T (P_14.Global_Var);
29 end if;
30end R_14;
Bodies and Proof
Assert, Assume, Check contracts
Assert (in loop) contract
The following example demonstrates how the SPARK 2005 assert annotation is used inside a loop as a loop invariant. It cuts the loop and on each iteration of the loop the list of existing hypotheses for the path is cleared. A verification condition is generated to prove that the assert expression is True, and the expression is the basis of the new hypotheses.
SPARK 2014 has a specific pragma for defining a loop invariant, pragma Loop_Invariant which is more sophisticated than the SPARK 2005 assert annotation and often requires less conditions in the invariant expression than in SPARK 2005. As in SPARK 2005 a default loop invariant will be used if one is not provided which, often, may be sufficient to prove absence of run-time exceptions. Like all SPARK 2014 assertion expressions the loop invariant is executable.
Note in the example below the SPARK 2014 version proves absence of run-time exceptions without an explicit loop invariant being provided.
Specification in SPARK 2005:
1package Assert_Loop_05
2is
3 subtype Index is Integer range 1 .. 10;
4 type A_Type is Array (Index) of Integer;
5
6 function Value_present (A: A_Type; X : Integer) return Boolean;
7 --# return for some M in Index => (A (M) = X);
8end Assert_Loop_05;
Body in SPARK 2005:
1package body Assert_Loop_05
2is
3 function Value_Present (A: A_Type; X : Integer) return Boolean
4 is
5 I : Index := Index'First;
6 begin
7 while A (I) /= X and I < Index'Last loop
8 --# assert I < Index'Last and
9 --# (for all M in Index range Index'First .. I => (A (M) /= X));
10 I := I + 1;
11 end loop;
12 return A (I) = X;
13 end Value_Present;
14end Assert_Loop_05;
Specification in SPARK 2014:
1package Assert_Loop_14
2 with SPARK_Mode
3is
4 subtype Index is Integer range 1 .. 10;
5 type A_Type is Array (Index) of Integer;
6
7 function Value_present (A : A_Type; X : Integer) return Boolean
8 with Post => Value_present'Result = (for some M in Index => A (M) = X);
9end Assert_Loop_14;
Body in SPARK 2014:
1package body Assert_Loop_14
2 with SPARK_Mode
3is
4 function Value_Present (A : A_Type; X : Integer) return Boolean is
5 I : Index := Index'First;
6 begin
7 while A (I) /= X and I < Index'Last loop
8 pragma Loop_Variant (Increases => I);
9 pragma Loop_Invariant
10 (I < Index'Last
11 and (for all M in Index'First .. I => A (M) /= X));
12 I := I + 1;
13 end loop;
14
15 return A (I) = X;
16 end Value_Present;
17end Assert_Loop_14;
Assert (no loop) contract
While not in a loop, the SPARK 2005 assert annotation maps to pragma Assert_And_Cut in SPARK 2014. Both the assert annotation and pragma assert clear the list of hypotheses on the path, generate a verification condition to prove the assertion expression and use the assertion expression as the basis of the new hypotheses.
Assume contract
The following example illustrates use of an Assume annotation. The assumed expression does not generate a verification condition and is not proved (although it is executed in SPARK 2014 if assertion expressions are not ignored at run-time).
In this example, the Assume annotation is effectively being used to implement the SPARK 2005 Always_Valid attribute.
Specification for Assume annotation in SPARK 2005:
1package Input_Port
2 --# own in Inputs;
3is
4 procedure Read_From_Port(Input_Value : out Integer);
5 --# global in Inputs;
6 --# derives Input_Value from Inputs;
7
8end Input_Port;
Body for Assume annotation in SPARK 2005:
1with System.Storage_Elements;
2package body Input_Port
3is
4
5 Inputs : Integer;
6 for Inputs'Address use System.Storage_Elements.To_Address (16#CAFE0#);
7 pragma Volatile (Inputs);
8
9 procedure Read_From_Port(Input_Value : out Integer)
10 is
11 begin
12 --# assume Inputs in Integer;
13 Input_Value := Inputs;
14 end Read_From_Port;
15
16end Input_Port;
Specification for Assume annotation in SPARK 2014:
1package Input_Port
2 with SPARK_Mode,
3 Abstract_State => (State_Inputs with External => Async_Writers)
4is
5 procedure Read_From_Port(Input_Value : out Integer)
6 with Global => (Input => State_Inputs),
7 Depends => (Input_Value => State_Inputs);
8end Input_Port;
Body for Assume annotation in SPARK 2014:
1with System.Storage_Elements;
2
3package body Input_Port
4 with SPARK_Mode,
5 Refined_State => (State_Inputs => Inputs)
6is
7 Inputs : Integer
8 with Volatile,
9 Async_Writers,
10 Address => System.Storage_Elements.To_Address (16#CAFE0#);
11
12 procedure Read_From_Port(Input_Value : out Integer)
13 with Refined_Global => (Input => Inputs),
14 Refined_Depends => (Input_Value => Inputs)
15 is
16 begin
17 Input_Value := Inputs;
18 pragma Assume(Input_Value in Integer);
19 end Read_From_Port;
20end Input_Port;
Check contract
The SPARK 2005 check annotation is replaced by pragma assert in SPARK 2014. This annotation generates a verification condition to prove the checked expression and adds the expression as a new hypothesis to the list of existing hypotheses.
Specification for Check annotation in SPARK 2005:
1package Check_05
2is
3 subtype Small is Integer range 1 .. 10;
4 subtype Big is Integer range 1 .. 21;
5
6 procedure Compare(A, B : in Small; C : in out Big);
7end Check_05;
Body for Check annotation in SPARK 2005:
1package body Check_05
2is
3 procedure Compare(A, B : in Small; C : in out Big)
4 is
5 begin
6 if (A + B >= C) then
7 C := A;
8 C := C + B;
9 C := C + 1;
10 end if;
11 --# check A + B < C;
12 end Compare;
13end Check_05;
Specification for Check annotation in SPARK 2014:
1package Check_14
2 with SPARK_Mode
3is
4 subtype Small is Integer range 1 .. 10;
5 subtype Big is Integer range 1 .. 21;
6
7 procedure Compare (A, B : in Small; C : in out Big);
8end Check_14;
Body for Check annotation in SPARK 2014:
1package body Check_14
2 with SPARK_Mode
3is
4 procedure Compare(A, B : in Small; C : in out Big) is
5 begin
6 if A + B >= C then
7 C := A;
8 C := C + B;
9 C := C + 1;
10 end if;
11 pragma Assert (A + B < C);
12 end Compare;
13end Check_14;
Assert used to control path explosion
This capability is in general not needed with the SPARK 2014 toolset where path explosion is handled automatically. In the rare cases where this is needed you can use pragma Assert_And_Cut.
Other Contracts and Annotations
Always_Valid assertion
See section Input driver using 'Tail in a contract for use of an assertion involving the Always_Valid attribute.
Rule declaration annotation
See section Proof types and proof functions.
Proof types and proof functions
The following example gives pre- and postconditions on operations that act upon the concrete representation of an abstract own variable. This means that proof functions and proof types are needed to state those pre- and postconditions. In addition, it gives an example of the use of a rule declaration annotation - in the body of procedure Initialize - to introduce a rule related to the components of a constant record value.
SPARK 2014 does not have a direct equivalent of proof types and proof functions. State abstractions cannot have a type and all functions in SPARK 2014 are Ada functions. Functions may be defined to be ghost functions which means that they can only be called within an assertion expression such as a pre or postcondition. Assertion expressions may be executed or ignored at run-time and if they are ignored Ghost functions behave much like SPARK 2005 proof functions.
Rule declaration annotations for structured constants are not required in SPARK 2014.
The SPARK 2005 version of the example given below will require user defined proof rules to discharge the proofs because refined definitions of some of the proof functions cannot be provided as they would have different formal parameters. The SPARK 2014 version does not suffer from this problem as functions called within assertion expressions may have global items.
Specification in SPARK 2005:
1package Stack
2--# own State : Abstract_Stack;
3is
4 -- It is not possible to specify that the stack will be
5 -- initialized to empty except by having an initialization
6 -- subprogram called during program execution (as opposed to
7 -- package elaboration).
8
9 -- Proof functions to indicate whether or not the Stack is empty
10 -- and whether or not it is full.
11 --# type Abstract_Stack is abstract;
12
13 --# function Max_Stack_Size return Natural;
14
15 -- Proof function to give the number of elements on the stack.
16 --# function Count(Input : Abstract_Stack) return Natural;
17
18 -- Proof function returns the Nth entry on the stack.
19 -- Stack_Entry (Count (State)) is the top of stack
20 --# function Stack_Entry (N : Natural; S : Abstract_Stack) return Integer;
21 --# pre N in 1 .. Count (S);
22 -- A refined version of this function cannot be written because
23 -- the abstract view has a formal parameter of type Abstract_Stack
24 -- whereas the refined view would not have this parameter but use
25 -- a global. A user defined proof rule would be required to define
26 -- this function. Alternatively, it could be written as an Ada
27 -- function where the the global and formal parameter views would
28 -- be available. However, the function would then be callable and
29 -- generate implementation code.
30
31 --# function Is_Empty(Input : Abstract_Stack) return Boolean;
32 --# return Count (Input) = 0;
33
34 --# function Is_Full(Input : Abstract_Stack) return Boolean;
35 --# return Count (Input) = Max_Stack_Size;
36
37 -- The precondition requires the stack is not full when a value, X,
38 -- is pushed onto it.
39 -- The postcondition indicates that the count of the stack will be
40 -- incremented after a push and therefore the stack will be non-empty.
41 -- The item X is now the top of the stack.
42 procedure Push(X : in Integer);
43 --# global in out State;
44 --# pre not Is_Full(State);
45 --# post Count (State) = Count (State~) + 1 and
46 --# Count (State) <= Max_Stack_Size and
47 --# Stack_Entry (Count (State), State) = X;
48
49 -- The precondition requires the stack is not empty when we
50 -- pull a value from it.
51 -- The postcondition indicates the stack count is decremented.
52 procedure Pop (X : out Integer);
53 --# global in out State;
54 --# pre not Is_Empty (State);
55 --# post Count (State) = Count (State~) - 1;
56
57 -- Procedure that swaps the first two elements in a stack.
58 procedure Swap2;
59 --# global in out State;
60 --# pre Count(State) >= 2;
61 --# post Count(State) = Count(State~) and
62 --# Stack_Entry (Count (State), State) =
63 --# Stack_Entry (Count (State) - 1, State~) and
64 --# Stack_Entry (Count (State) - 1, State) =
65 --# Stack_Entry (Count (State), State~);
66
67 -- Initializes the Stack.
68 procedure Initialize;
69 --# global out State;
70 --# post Is_Empty (State);
71end Stack;
Body in SPARK 2005:
1package body Stack
2--# own State is My_Stack;
3is
4 Stack_Size : constant := 100;
5 type Pointer_Range is range 0 .. Stack_Size;
6 subtype Index_Range is Pointer_Range range 1..Stack_Size;
7 type Vector is array(Index_Range) of Integer;
8
9 type Stack_Type is record
10 S : Vector;
11 Pointer : Pointer_Range;
12 end record;
13
14 Initial_Stack : constant Stack_Type :=
15 Stack_Type'(S => Vector'(others => 0),
16 Pointer => 0);
17
18 My_Stack : Stack_Type;
19
20 procedure Push(X : in Integer)
21 --# global in out My_Stack;
22 --# pre My_Stack.Pointer < Stack_Size;
23 is
24 begin
25 My_Stack.Pointer := My_Stack.Pointer + 1;
26 My_Stack.S(My_Stack.Pointer) := X;
27 end Push;
28
29 procedure Pop (X : out Integer)
30 --# global in out My_Stack;
31 --# pre My_Stack.Pointer >= 1;
32 is
33 begin
34 X := My_Stack.S (My_Stack.Pointer);
35 My_Stack.Pointer := My_Stack.Pointer - 1;
36 end Pop;
37
38 procedure Swap2
39 --# global in out My_Stack;
40 --# post My_Stack.Pointer = My_Stack~.Pointer;
41 is
42 Temp : Integer;
43 begin
44 Temp := My_Stack.S (1);
45 My_Stack.S (1) := My_Stack.S (2);
46 My_Stack.S (2) := Temp;
47 end Swap2;
48
49 procedure Initialize
50 --# global out My_Stack;
51 --# post My_Stack.Pointer = 0;
52 is
53 --# for Initial_Stack declare Rule;
54 begin
55 My_Stack := Initial_Stack;
56 end Initialize;
57end Stack;
Specification in SPARK 2014
1package Stack
2 with SPARK_Mode,
3 Abstract_State => State,
4 Initializes => State,
5 Initial_Condition => Is_Empty
6is
7 -- In SPARK 2014 we can specify an initial condition for the
8 -- elaboration of a package and so initialization may be done
9 -- during the elaboration of the package Stack, rendering the need
10 -- for an initialization procedure unnecessary.
11
12 -- Abstract states do not have types in SPARK 2014 they can only
13 -- be directly referenced in Global and Depends aspects.
14
15 -- Proof functions are actual functions but they may have the
16 -- convention Ghost meaning that they can only be called from
17 -- assertion expressions, e.g., pre and postconditions
18 function Max_Stack_Size return Natural
19 with Ghost;
20
21 -- Returns the number of elements on the stack
22 function Count return Natural
23 with Global => (Input => State),
24 Ghost;
25
26 -- Returns the Nth entry on the stack. Stack_Entry (Count) is the
27 -- top of stack
28 function Stack_Entry (N : Natural) return Integer
29 with Global => (Input => State),
30 Pre => N in 1 .. Count,
31 Ghost;
32 -- A body (refined) version of this function can (must) be
33 -- provided in the body of the package.
34
35 function Is_Empty return Boolean is (Count = 0)
36 with Global => State,
37 Ghost;
38
39 function Is_Full return Boolean is (Count = Max_Stack_Size)
40 with Global => State,
41 Ghost;
42
43 -- The precondition requires the stack is not full when a value,
44 -- X, is pushed onto it. Functions with global items (Is_Full
45 -- with global State in this case) can be called in an assertion
46 -- expression such as the precondition here. The postcondition
47 -- indicates that the count of the stack will be incremented after
48 -- a push and therefore the stack will be non-empty. The item X
49 -- is now the top of the stack.
50 procedure Push (X : in Integer)
51 with Global => (In_Out => State),
52 Pre => not Is_Full,
53 Post => Count = Count'Old + 1 and
54 Count <= Max_Stack_Size and
55 Stack_Entry (Count) = X;
56
57 -- The precondition requires the stack is not empty when we pull a
58 -- value from it. The postcondition indicates the stack count is
59 -- decremented.
60 procedure Pop (X : out Integer)
61 with Global => (In_Out => State),
62 Pre => not Is_Empty,
63 Post => Count = Count'Old - 1;
64
65 -- Procedure that swaps the top two elements in a stack.
66 procedure Swap2
67 with Global => (In_Out => State),
68 Pre => Count >= 2,
69 Post => Count = Count'Old and
70 Stack_Entry (Count) = Stack_Entry (Count - 1)'Old and
71 Stack_Entry (Count - 1) = Stack_Entry (Count)'Old;
72end Stack;
Body in SPARK 2014:
1package body Stack
2 with SPARK_Mode,
3 Refined_State => (State => My_Stack)
4is
5 Stack_Size : constant := 100;
6 type Pointer_Range is range 0 .. Stack_Size;
7 subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
8 type Vector is array(Index_Range) of Integer;
9
10 type Stack_Type is record
11 S : Vector;
12 Pointer : Pointer_Range;
13 end record;
14
15 Initial_Stack : constant Stack_Type :=
16 Stack_Type'(S => Vector'(others => 0),
17 Pointer => 0);
18 My_Stack : Stack_Type;
19
20 function Max_Stack_Size return Natural is (Stack_Size);
21
22 function Count return Natural is (Natural (My_Stack.Pointer))
23 with Refined_Global => My_Stack;
24
25 function Stack_Entry (N : Natural) return Integer is
26 (My_Stack.S (Index_Range (N)))
27 with Refined_Global => My_Stack;
28
29
30 procedure Push(X : in Integer)
31 with Refined_Global => (In_Out => My_Stack)
32 is
33 begin
34 My_Stack.Pointer := My_Stack.Pointer + 1;
35 My_Stack.S(My_Stack.Pointer) := X;
36 end Push;
37
38 procedure Pop (X : out Integer)
39 with Refined_Global => (In_Out => My_Stack)
40 is
41 begin
42 X := My_Stack.S (My_Stack.Pointer);
43 My_Stack.Pointer := My_Stack.Pointer - 1;
44 end Pop;
45
46 procedure Swap2
47 with Refined_Global => (In_Out => My_Stack)
48 is
49 Temp : Integer;
50 begin
51 Temp := My_Stack.S (My_Stack.Pointer);
52 My_Stack.S (My_Stack.Pointer) := My_Stack.S (My_Stack.Pointer - 1);
53 My_Stack.S (My_Stack.Pointer - 1) := Temp;
54 end Swap2;
55begin
56 My_Stack := Initial_Stack;
57end Stack;
Using an External Prover
One may wish to use an external prover such as Isabelle, with rules defining a ghost function written in the prover input language. This can be done in SPARK 2014 by denoting the ghost function as an Import in lieu of providing a body for it. Of course such ghost functions cannot be executed.
Specification in SPARK 2014 using an external prover:
1package Stack_External_Prover
2 with SPARK_Mode,
3 Abstract_State => State,
4 Initializes => State,
5 Initial_Condition => Is_Empty
6is
7 -- A Ghost function may be an Import which means that no body is
8 -- given in the SPARK 2014 code and the proof has to be discharged
9 -- by an external prover. Of course, such functions are not
10 -- executable.
11 function Max_Stack_Size return Natural
12 with Global => null,
13 Ghost,
14 Import;
15
16 -- Returns the number of elements on the stack
17 function Count return Natural
18 with Global => (Input => State),
19 Ghost,
20 Import;
21
22 -- Returns the Nth entry on the stack. Stack_Entry (Count) is the
23 -- top of stack
24 function Stack_Entry (N : Natural) return Integer
25 with Global => (Input => State),
26 Ghost,
27 Import;
28
29 function Is_Empty return Boolean
30 with Global => State,
31 Ghost,
32 Import;
33
34 function Is_Full return Boolean
35 with Global => State,
36 Ghost,
37 Import;
38
39 procedure Push (X : in Integer)
40 with Global => (In_Out => State),
41 Always_Terminates,
42 Pre => not Is_Full,
43 Post => Count = Count'Old + 1 and Count <= Max_Stack_Size and
44 Stack_Entry (Count) = X;
45
46 procedure Pop (X : out Integer)
47 with Global => (In_Out => State),
48 Always_Terminates,
49 Pre => not Is_Empty,
50 Post => Count = Count'Old - 1;
51
52 procedure Swap2
53 with Global => (In_Out => State),
54 Always_Terminates,
55 Pre => Count >= 2,
56 Post => Count = Count'Old and
57 Stack_Entry (Count) = Stack_Entry (Count - 1)'Old and
58 Stack_Entry (Count - 1) = Stack_Entry (Count)'Old;
59end Stack_External_Prover;
Quoting an Own Variable in a Contract
Sometimes it is necessary to reference an own variable (a state abstraction) in a contract. In SPARK 2005 this was achieved by declaring the own variable with a type, either concrete or abstract. As seen in Proof types and proof functions. Once the own variable has a type it can be used in a SPARK 2005 proof context.
A state abstraction in SPARK 2014 does not have a type. Instead, an Ada type to represent the abstract state is declared. A function which has the state abstraction as a global item is then declared which returns an object of the type. This function may have the same name as the state abstraction (the name is overloaded). References which appear to be the abstract state in an assertion expression are in fact calls to the overloaded function.
An example of this technique is given in the following example which is a version of the stack example given in Proof types and proof functions but with the post conditions extended to express the functional properties of the stack.
The extension requires the quoting of the own variable/state abstraction in the postcondition in order to state that the contents of the stack other than the top entries are not changed.
Specification in SPARK 2005:
1package Stack_Functional_Spec
2--# own State : Abstract_Stack;
3is
4 -- It is not possible to specify that the stack will be
5 -- initialized to empty except by having an initialization
6 -- subprogram called during program execution (as opposed to
7 -- package elaboration).
8
9 -- Proof functions to indicate whether or not the Stack is empty
10 -- and whether or not it is full.
11 --# type Abstract_Stack is abstract;
12
13 --# function Max_Stack_Size return Natural;
14
15 -- Proof function to give the number of elements on the stack.
16 --# function Count(Input : Abstract_Stack) return Natural;
17
18 -- Proof function returns the Nth entry on the stack.
19 -- Stack_Entry (Count (State)) is the top of stack
20 --# function Stack_Entry (S : Abstract_Stack; N : Natural) return Integer;
21 --# pre N in 1 .. Count (S);
22 -- A refined version of this function cannot be written because
23 -- the abstract view has a formal parameter of type Abstract_Stack
24 -- whereas the refined view would not have this parameter but use
25 -- a global. A user defined proof rule would be required to
26 -- define this function. Alternatively, it could be written as an
27 -- Ada function where the the global and formal parameter views
28 -- would be available. However, the function would then be
29 -- callable and generate implementation code.
30
31 --# function Is_Empty(Input : Abstract_Stack) return Boolean;
32 --# return Count (Input) = 0;
33
34 --# function Is_Full(Input : Abstract_Stack) return Boolean;
35 --# return Count (Input) = Max_Stack_Size;
36
37 -- The precondition requires the stack is not full when a value, X,
38 -- is pushed onto it.
39 -- Functions with global items (Is_Full with global State in this case)
40 -- can be called in an assertion expression such as the precondition here.
41 -- The postcondition indicates that the count of the stack will be
42 -- incremented after a push and therefore the stack will be non-empty.
43 -- The item X is now the top of the stack and the contents of the rest of
44 -- the stack are unchanged.
45 procedure Push(X : in Integer);
46 --# global in out State;
47 --# pre not Is_Full(State);
48 --# post Count (State) = Count (State~) + 1 and
49 --# Count (State) <= Max_Stack_Size and
50 --# Stack_Entry (State, Count (State)) = X and
51 --# (for all I in Natural range 1 .. Count (State~) =>
52 --# (Stack_Entry (State, I) = Stack_Entry (State~, I)));
53
54 -- The precondition requires the stack is not empty when we
55 -- pull a value from it.
56 -- The postcondition indicates that the X = the old top of stack,
57 -- the stack count is decremented, and the contents of the stack excluding
58 -- the old top of stack are unchanged.
59 procedure Pop (X : out Integer);
60 --# global in out State;
61 --# pre not Is_Empty (State);
62 --# post Count (State) = Count (State~) - 1 and
63 --# X = Stack_Entry (State~, Count (State~)) and
64 --# (for all I in Natural range 1 .. Count (State) =>
65 --# (Stack_Entry (State, I) = Stack_Entry (State~, I)));
66
67 -- The precondition requires that the stack has at least 2 entries
68 -- (Count >= 2).
69 -- The postcondition states that the top two elements of the stack are
70 -- transposed but the remainder of the stack is unchanged.
71 procedure Swap2;
72 --# global in out State;
73 --# pre Count(State) >= 2;
74 --# post Count(State) = Count(State~) and
75 --# Stack_Entry (State, Count (State)) =
76 --# Stack_Entry (State~, Count (State) - 1) and
77 --# Stack_Entry (State, Count (State) - 1) =
78 --# Stack_Entry (State~, Count (State)) and
79 --# (for all I in Natural range 1 .. Count (State) =>
80 --# (Stack_Entry (State, I) = Stack_Entry (State~, I)));
81
82 -- Initializes the Stack.
83 procedure Initialize;
84 --# global out State;
85 --# post Is_Empty (State);
86end Stack_Functional_Spec;
Body in SPARK 2005:
1package body Stack_Functional_Spec
2--# own State is My_Stack;
3is
4 Stack_Size : constant := 100;
5 type Pointer_Range is range 0 .. Stack_Size;
6 subtype Index_Range is Pointer_Range range 1..Stack_Size;
7 type Vector is array(Index_Range) of Integer;
8
9 type Stack_Type is
10 record
11 S : Vector;
12 Pointer : Pointer_Range;
13 end record;
14
15 Initial_Stack : constant Stack_Type :=
16 Stack_Type'(S => Vector'(others => 0),
17 Pointer => 0);
18
19 My_Stack : Stack_Type;
20
21 procedure Push(X : in Integer)
22 --# global in out My_Stack;
23 --# pre My_Stack.Pointer < Stack_Size;
24 is
25 begin
26 My_Stack.Pointer := My_Stack.Pointer + 1;
27 My_Stack.S(My_Stack.Pointer) := X;
28 end Push;
29
30 procedure Pop (X : out Integer)
31 --# global in out My_Stack;
32 --# pre My_Stack.Pointer >= 1;
33 is
34 begin
35 X := My_Stack.S (My_Stack.Pointer);
36 My_Stack.Pointer := My_Stack.Pointer - 1;
37 end Pop;
38
39 procedure Swap2
40 --# global in out My_Stack;
41 --# post My_Stack.Pointer = My_Stack~.Pointer;
42 is
43 Temp : Integer;
44 begin
45 Temp := My_Stack.S (1);
46 My_Stack.S (1) := My_Stack.S (2);
47 My_Stack.S (2) := Temp;
48 end Swap2;
49
50 procedure Initialize
51 --# global out My_Stack;
52 --# post My_Stack.Pointer = 0;
53 is
54 --# for Initial_Stack declare Rule;
55 begin
56 My_Stack := Initial_Stack;
57 end Initialize;
58
59end Stack_Functional_Spec;
Specification in SPARK 2014
1pragma Unevaluated_Use_Of_Old(Allow);
2package Stack_Functional_Spec
3 with SPARK_Mode,
4 Abstract_State => State,
5 Initializes => State,
6 Initial_Condition => Is_Empty
7is
8 -- Abstract states do not have types in SPARK 2014 but to provide
9 -- functional specifications it is sometimes necessary to refer to
10 -- the abstract state in an assertion expression such as a post
11 -- condition. To do this in SPARK 2014 an Ada type declaration is
12 -- required to represent the type of the abstract state, then a
13 -- function applied to the abstract state (as a global) can be
14 -- written which returns an object of the declared type.
15 type Stack_Type is private;
16
17 -- The Abstract_State name may be overloaded by the function which
18 -- represents it in assertion expressions.
19 function State return Stack_Type
20 with Global => State;
21
22 function Max_Stack_Size return Natural
23 with Ghost;
24
25 -- Returns the number of elements on the stack
26 -- A function may have a formal parameter (or return a value)
27 -- of the abstract state.
28 function Count (S : Stack_Type) return Natural
29 with Ghost;
30
31 -- Returns the Nth entry on the stack.
32 -- Stack_Entry (S, Count (S)) is the top of stack
33 function Stack_Entry (S : Stack_Type; N : Natural) return Integer
34 with Pre => N in 1 .. Count (S),
35 Ghost;
36
37 -- The ghost function Count can be called in the function
38 -- expression because Is_Empty is also a ghost function.
39 function Is_Empty return Boolean is (Count (State) = 0)
40 with Global => State,
41 Ghost;
42
43 function Is_Full return Boolean is (Count(State) = Max_Stack_Size)
44 with Global => State,
45 Ghost;
46
47 -- The precondition requires the stack is not full when a value, X,
48 -- is pushed onto it.
49 -- Functions with global items (Is_Full with global State in this case)
50 -- can be called in an assertion expression such as the precondition here.
51 -- The postcondition indicates that the count of the stack will be
52 -- incremented after a push and therefore the stack will be non-empty.
53 -- The item X is now the top of the stack and the contents of the rest of
54 -- the stack are unchanged.
55 procedure Push (X : in Integer)
56 with Global => (In_Out => State),
57 Pre => not Is_Full,
58 Post => Count (State) = Count (State'Old) + 1 and
59 Count (State) <= Max_Stack_Size and
60 Stack_Entry (State, Count (State)) = X and
61 (for all I in 1 .. Count (State'Old) =>
62 Stack_Entry (State, I) = Stack_Entry (State'Old, I));
63
64 -- The precondition requires the stack is not empty when we
65 -- pull a value from it.
66 -- The postcondition indicates that the X = the old top of stack,
67 -- the stack count is decremented, and the contents of the stack excluding
68 -- the old top of stack are unchanged.
69 procedure Pop (X : out Integer)
70 with Global => (In_Out => State),
71 Pre => not Is_Empty,
72 Post => Count (State) = Count (State'Old) - 1 and
73 X = Stack_Entry (State'Old, Count (State'Old)) and
74 (for all I in 1 .. Count (State) =>
75 Stack_Entry (State, I) = Stack_Entry (State'Old, I));
76
77 -- The precondition requires that the stack has at least 2 entries
78 -- (Count >= 2).
79 -- The postcondition states that the top two elements of the stack are
80 -- transposed but the remainder of the stack is unchanged.
81 procedure Swap2
82 with Global => (In_Out => State),
83 Pre => Count (State) >= 2,
84 Post => Count(State) = Count (State'Old) and
85 Stack_Entry (State, Count (State)) =
86 Stack_Entry (State'Old, Count (State) - 1) and
87 Stack_Entry (State, Count (State) - 1) =
88 Stack_Entry (State'Old, Count (State)) and
89 (for all I in 1 .. Count (State) - 2 =>
90 Stack_Entry (State, I) = Stack_Entry (State'Old, I));
91
92private
93 -- The full type declarion used to represent the abstract state.
94 Stack_Size : constant := 100;
95 type Pointer_Range is range 0 .. Stack_Size;
96 subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
97 type Vector is array(Index_Range) of Integer;
98
99 type Stack_Type is record
100 S : Vector;
101 Pointer : Pointer_Range;
102 end record;
103end Stack_Functional_Spec;
Body in SPARK 2014:
1package body Stack_Functional_Spec
2 with SPARK_Mode,
3 Refined_State => (State => My_Stack)
4is
5 Initial_Stack : constant Stack_Type :=
6 Stack_Type'(S => Vector'(others => 0),
7 Pointer => 0);
8
9 -- In this example the type used to represent the state
10 -- abstraction and the actual type used in the implementation are
11 -- the same, but they need not be. For instance S and Pointer
12 -- could have been declared as distinct objects rather than
13 -- composed into a record. Where the type representing the
14 -- abstract state and the implementation of that state are
15 -- different the function representing the abstract state has to
16 -- convert implementation representation into the abstract
17 -- representation. For instance, if S and Pointer were distinct
18 -- objects the function State would have to return (S => S,
19 -- Pointer => Pointer).
20 My_Stack : Stack_Type;
21
22 -- No conversion necessary as the abstract and implementation type
23 -- is the same.
24 function State return Stack_Type is (My_Stack)
25 with Refined_Global => My_Stack;
26
27 function Max_Stack_Size return Natural is (Stack_Size);
28
29 function Count (S : Stack_Type) return Natural is (Natural (S.Pointer));
30
31 function Stack_Entry (S : Stack_Type; N : Natural) return Integer is
32 (S.S (Index_Range (N)));
33
34 procedure Push(X : in Integer)
35 with Refined_Global => (In_Out => My_Stack)
36 is
37 begin
38 My_Stack.Pointer := My_Stack.Pointer + 1;
39 My_Stack.S(My_Stack.Pointer) := X;
40 end Push;
41
42 procedure Pop (X : out Integer)
43 with Refined_Global => (In_Out => My_Stack)
44 is
45 begin
46 X := My_Stack.S (My_Stack.Pointer);
47 My_Stack.Pointer := My_Stack.Pointer - 1;
48 end Pop;
49
50 procedure Swap2
51 with Refined_Global => (In_Out => My_Stack)
52 is
53 Temp : Integer;
54 begin
55 Temp := My_Stack.S (My_Stack.Pointer);
56 My_Stack.S (My_Stack.Pointer) := My_Stack.S (My_Stack.Pointer - 1);
57 My_Stack.S (My_Stack.Pointer - 1) := Temp;
58 end Swap2;
59begin
60 My_Stack := Initial_Stack;
61end Stack_Functional_Spec;
Main_Program annotation
This annotation isn’t needed. Currently any parameterless procedure declared at library-level is considered as a potential main program and analyzed as such.
Update Expressions
SPARK 2005 has update expressions for updating records and arrays. They can only be used in SPARK 2005 proof contexts.
The equivalent in SPARK 2014 is a delta aggregate. This can be used in any Ada expression.
Specification in SPARK 2005:
1package Update_Examples
2is
3 type Rec is record
4 X, Y : Integer;
5 end record;
6
7 type Index is range 1 ..3;
8
9 type Arr is array (Index) of Integer;
10
11 type Arr_2D is array (Index, Index) of Integer;
12
13 type Nested_Rec is record
14 A : Integer;
15 B : Rec;
16 C : Arr;
17 D : Arr_2D;
18 end record;
19
20 type Nested_Arr is array (Index) of Nested_Rec;
21
22 -- Simple record update
23 procedure P1 (R : in out Rec);
24 --# post R = R~ [X => 1];
25
26 -- Simple 1D array update
27 procedure P2 (A : in out Arr);
28 --# post A = A~ [1 => 2];
29
30 -- 2D array update
31 procedure P3 (A2D : in out Arr_2D);
32 --# post A2D = A2D~ [1, 1 => 1;
33 --# 2, 2 => 2;
34 --# 3, 3 => 3];
35
36 -- Nested record update
37 procedure P4 (NR : in out Nested_Rec);
38 --# post NR = NR~ [A => 1;
39 --# B => NR~.B [X => 1];
40 --# C => NR~.C [1 => 5]];
41
42 -- Nested array update
43 procedure P5 (NA : in out Nested_Arr);
44 --# post NA = NA~ [1 => NA~ (1) [A => 1;
45 --# D => NA~ (1).D [2, 2 => 0]];
46 --# 2 => NA~ (2) [B => NA~ (2).B [X => 2]];
47 --# 3 => NA~ (3) [C => NA~ (3).C [1 => 5]]];
48end Update_Examples;
Specification in SPARK 2014
1package Update_Examples
2 with SPARK_Mode
3is
4 type Rec is record
5 X, Y : Integer;
6 end record;
7
8 type Arr is array (1 .. 3) of Integer;
9
10 type Nested_Rec is record
11 A : Integer;
12 B : Rec;
13 C : Arr;
14 end record;
15
16 type Nested_Arr is array (1 .. 3) of Nested_Rec;
17
18 -- Simple record update
19 procedure P1 (R : in out Rec)
20 with Post => R = (R'Old with delta X => 1);
21 -- this is equivalent to:
22 -- R = (X => 1,
23 -- Y => R'Old.Y)
24
25 -- Simple 1D array update
26 procedure P2 (A : in out Arr)
27 with Post => A = (A'Old with delta 1 => 2);
28 -- this is equivalent to:
29 -- A = (1 => 2,
30 -- 2 => A'Old (2),
31 -- 3 => A'Old (3));
32
33 -- Nested record update
34 procedure P3 (NR : in out Nested_Rec)
35 with Post => NR = (NR'Old with delta A => 1,
36 B => (NR'Old.B with delta X => 1),
37 C => (NR'Old.C with delta 1 => 5));
38 -- this is equivalent to:
39 -- NR = (A => 1,
40 -- B.X => 1,
41 -- B.Y => NR'Old.B.Y,
42 -- C (1) => 5,
43 -- C (2) => NR'Old.C (2),
44 -- C (3) => NR'Old.C (3))
45
46 -- Nested array update
47 procedure P4 (NA : in out Nested_Arr)
48 with Post =>
49 NA = (NA'Old with delta
50 1 => (NA'Old (1) with delta A => 1),
51 2 => (NA'Old (2) with delta
52 B => (NA'Old (2).B with delta X => 2)),
53 3 => (NA'Old (3) with delta
54 C => (NA'Old (3).C with delta 1 => 5)));
55 -- this is equivalent to:
56 -- NA = (1 => (A => 1,
57 -- B => NA'Old (1).B,
58 -- C => NA'Old (1).C),
59 -- 2 => (B.X => 2,
60 -- B.Y => NA'Old (2).B.Y,
61 -- A => NA'Old (2).A,
62 -- C => NA'Old (2).C),
63 -- 3 => (C => (1 => 5,
64 -- 2 => NA'Old (3).C (2),
65 -- 3 => NA'Old (3).C (3)),
66 -- A => NA'Old (3).A,
67 -- B => NA'Old (3).B));
68
69end Update_Examples;
Value of Variable on Entry to a Loop
In SPARK 2005 the entry value of a for loop variable variable, X, can be referenced using the notation X%. This notation is required frequently when the variable is referenced in a proof context within the loop. Often it is needed to state that the value of X is not changed within the loop by stating X = X%. This notation is restricted to a variable which defines the lower or upper range of a for loop.
SPARK 2014 has a more general scheme whereby the loop entry value of any variable can be denoted within any sort of loop using the ‘Loop_Entry attribute. However, its main use is not for showing that the value of a for loop variable has not changed as the SPARK 2014 tools are able to determine this automatically. Rather it is used instead of ~ in loops because the attribute ‘Old is only permitted in postconditions (including Contract_Cases).
Specification in SPARK 2005:
1package Loop_Entry
2is
3
4 subtype ElementType is Natural range 0..1000;
5 subtype IndexType is Positive range 1..100;
6 type ArrayType is array (IndexType) of ElementType;
7
8 procedure Clear (A: in out ArrayType; L,U: in IndexType);
9 --# derives A from A, L, U;
10 --# post (for all N in IndexType range L..U => (A(N) = 0)) and
11 --# (for all N in IndexType => ((N<L or N>U) -> A(N) = A~(N)));
12
13end Loop_Entry;
Body in SPARK 2005:
1package body Loop_Entry
2is
3
4 procedure Clear (A: in out ArrayType; L,U: in IndexType)
5 is
6 begin
7 for I in IndexType range L..U loop
8 A(I) := 0;
9 --# assert (for all N in IndexType range L..I => (A(N) = 0)) and
10 --# (for all N in IndexType => ((N<L or N>I) -> A(N) = A~(N))) and
11 --# U = U% and L <= I;
12 -- Note U = U% is required to show that the vaule of U does not change
13 -- within the loop.
14 end loop;
15 end Clear;
16
17end Loop_Entry;
Specification in SPARK 2014:
1pragma SPARK_Mode (On);
2package Loop_Entry
3is
4
5 subtype ElementType is Natural range 0..1000;
6 subtype IndexType is Positive range 1..100;
7 type ArrayType is array (IndexType) of ElementType;
8
9 procedure Clear (A: in out ArrayType; L,U: in IndexType)
10 with Depends => (A => (A, L, U)),
11 Post => (for all N in L..U => A(N) = 0) and
12 (for all N in IndexType =>
13 (if N<L or N>U then A(N) = A'Old(N)));
14
15end Loop_Entry;
Body in SPARK 2014:
1pragma SPARK_Mode (On);
2package body Loop_Entry
3is
4
5 procedure Clear (A: in out ArrayType; L,U: in IndexType)
6 is
7 begin
8 for I in IndexType range L..U loop
9 A(I) := 0;
10 pragma Loop_Invariant ((for all N in L..I => (A(N) = 0)) and
11 (for all N in IndexType =>
12 (if N < L or N > I then A(N) = A'Loop_Entry(N))));
13 -- Note it is not necessary to show that the vaule of U does not change
14 -- within the loop.
15 -- However 'Loop_Entry must be used rather than 'Old.
16 end loop;
17 end Clear;
18
19end Loop_Entry;