SPARK 2014 Rationale: Data Dependencies
by Florian Schanda –
I claim that aspect Global is extremely easy to use. In order to figure out whether I am right or wrong, lets conduct an experiment. Without having explained anything about how aspect Global works I will give you the specifications of three procedures and also the code of the Main that calls them. You will then have to guess if the Main will behave predictably or not. If you guess correctly, then my initial statement was correct (otherwise, ... oh well 
). So, here we go:
package Guess_The_Order is
Global_Variable : Integer;
procedure Print with
Global => (Input => Global_Variable);
procedure Sub (X, Y : in Integer) with
Global => (In_Out => Global_Variable);
procedure Add (X, Y : in Integer) with
Global => (Output => Global_Variable);
end Guess_The_Order;
with Guess_The_Order;
procedure Main is
begin
Sub (6, 1);
Add (2, 3);
Print;
end Main;The main program will produce unpredictable results because procedure Sub tries to read Global_Var before it has been initialized! The correct order would be, call Add first, Sub second and Print last. The Global aspect on procedure Add says that Global_Variable will be set by the subprogram. Procedure Sub's contract says that Global_Variable will be both read (which is what causes the problem) and written. Procedure Print only reads Global_Variable and presumably does some kind of printing.
Regardless of whether you guessed correctly or not, if you want to learn some more about how aspect Global works, read on! 
The Global aspect helps us in two different ways. It ensures that:
- ALL global variables mentioned by the aspect, and ONLY them, will be used by the subprogram and
- global variables that are meant as inputs are not updated and global variables that are meant as outputs are NOT read before they are set.
The following four modes inform us of the way in which the subprogram interacts with its global variables:
- Input: A global variable of this mode can NOT have its value updated. The global variable can and HAS TO be read. This means that there has to be at least one execution path of the subprogram where the global is read. In essence, if we say that something is an Input, then it is an Input!
- Output: Global variables of this mode can NOT have their values read before the subprogram has set them. Furthermore, their values have to be set in ALL execution paths of the subprogram. This means that by the end of the subprogram the value of the global will always be set to something.
- In_Out: There has to be at least one execution path that reads the initial value of the global variable and one path that updates it.
- Proof_In: The value of the global variable can only be mentioned inside proof related annotations. Consequently, no outputs of the subprogram can ever be affected by a such a global variable. This mode allows us to use globals to check that certain properties are true for our subprogram but it also ensures that we did NOT accidentally affect the outputs of the subprogram while doing our checks.
When a mode is not specified, the tools assume a default mode of "Input". Conceptually, the first 3 modes are very similar to modes "in", "out" and "in out" of formal parameters.
Enforcing that NO global variables are used
When a subprogram is annotated with a "Global => null" contract, the tools will ensure that NO global variables are used by the subprogram. Be careful, having no Global contract is not the same as having a null Global contract (i.e. Global => null). In the absence of a Globalcontract, the tools will generate an implicit Global contract based on the subprogram's body, they will assume that to be the correct contract and will propagate it to all callers of the subprogram.
Correct Examples
package Correct_Globals
with SPARK_Mode
is
Everything_OK : Boolean := True;
Global_Var : Natural := 1;
Backup_Global_Var : Natural := 1;
procedure Increase_1 (X : in out Natural) with
Global => (Input => Global_Var);
-- Same as: "with Global => Global_Var;"
procedure Increase_2 (X : in out Natural) with
Global => null;
-- Cannot use any global variables here.
procedure Increase_Global_Var (X : Natural) with
Global => (In_Out => Global_Var,
Output => Backup_Global_Var,
Proof_In => Everything_OK);
-- Everything_OK can only appear in proof-related annotations.
end Correct_Globals;
package body Correct_Globals
with SPARK_Mode
is
procedure Increase_1 (X : in out Natural) is
begin
X := X + Global_Var;
end Increase_1;
procedure Increase_2 (X : in out Natural) is
begin
X := X + 1;
end Increase_2;
procedure Increase_Global_Var (X : Natural) is
begin
pragma Assert (Everything_OK); -- Some assertion...
Backup_Global_Var := Global_Var;
Global_Var := Global_Var + X;
end Increase_Global_Var;
end Correct_Globals;Incorrect Examples
package Incorrect_Globals
with SPARK_Mode
is
Global_Var : Integer;
procedure Read_Global_Variable (X : out Integer) with
Global => Global_Var;
procedure Update_Global_Var (X : Integer) with
Global => (Output => Global_Var);
function Increase (X : Integer) return Integer with
Global => null;
end Incorrect_Globals;
package body Incorrect_Globals
with SPARK_Mode
is
procedure Read_Global_Variable (X : out Integer) is
begin
X := Global_Var;
Global_Var := Global_Var + 1; -- Global_Var is of mode "Input"
-- The error message generated by the tools is:
-- "Global_Var" must be a global output of "Read_Global_Variable"
end Read_Global_Variable;
procedure Update_Global_Var (X : Integer) is
begin
if X < 0 then
Global_Var := -1 * X;
elsif X > 0 then
Global_Var := X;
end if;
-- When X = 0, Global_Var is not being set. So it's Global mode
-- should have been In_Out. Another way to look at it is as follows.
-- A mode of "Output" means that the global variable is ALWAYS set
-- while a mode of "In_Out" means that the variable is set
-- SOMETIMES BUT NOT ALWAYS. The warnigs printed by the tools here is:
-- warning: "Global_Var" might not be initialized
end Update_Global_Var;
function Increase (X : Integer) return Integer is
(if X < 0
then X + 1
else X + Global_Var);
-- The error message generated by the tools is:
-- "Global_Var" must be listed in the Global aspect of "Increase"
end Incorrect_Globals;Generated Globals
When a user-provided contract is available, the tools will attempt to verify its validity and report back in case of a contradiction. As said before, in the absence of a user-provided contract, the tools generate a contract based on the body of the subprogram, they then consider this to be the "correct" contract and use it to verify any user-provided contracts.
package Generated_Globals
with SPARK_Mode
is
Global_Var : Integer := 1;
procedure Without_Contract (X : out Integer);
-- Based on the body, the tools will compute a global contract that will
-- say that Global_Var is a global input.
procedure With_Correct_Contract (X : out Integer) with
Global => Global_Var;
procedure With_Incorrect_Contract (X : out Integer) with
Global => null;
end Generated_Globals;
package body Generated_Globals
with SPARK_Mode
is
procedure Without_Contract (X : out Integer) is
begin
X := Global_Var;
end Without_Contract;
procedure With_Correct_Contract (X : out Integer) is
begin
Without_Contract (X);
-- The computed Global contract verifies the validity of
-- the user-provided contract of procedure With_Contract.
end With_Correct_Contract;
procedure With_Incorrect_Contract (X : out Integer) is
begin
Without_Contract (X);
-- The computed Global contract contradicts the user-provided contract
-- of procedure With_Contract. Due to the mismatch, the following
-- error is generated:
-- "Global_Var" must be listed in the Global aspect of
-- "With_Incorrect_Contract"
end With_Incorrect_Contract;
end Generated_Globals;Conclusion
In his book "Better Embedded Systems SW" Phil Koopman says: "The main problem with using global variables is that they create implicit couplings among various pieces of the program (various routines might set or modify a variable, while several more routines might read it). Those couplings are not well represented in the software design, and are not explicitly represented in the implementation language. This type of opaque data coupling among modules results in difficult to find and hard to understand bugs." We don't have this in SPARK, thanks to the Global aspect!