SPARK 2014 Rationale: Data Dependencies

by in Language, Formal Verification, Design Method – March 18, 2014

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 cheeky). 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! smiley

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 Global contract, 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! smiley

Links

comments powered by Disqus