AdaCore Blog

SPARK 2014 Rationale: Global State

by Yannick Moy

Global variables can be easily subverted to cater for poor design and quick-and-dirty workarounds, to a point that they are considered as evil in some professional environments. Their extended scope and lifetime is a source of programming errors: as they are sometimes initialized far from their definition, it's easy to forget to initialize them completely; as they are accessible from many points in the program, they can be used to implement conflicting needs; as they may be modified through different subprograms, their correct use may require specific sequences of calls, etc.

SPARK 2014 provides a way to define abstractly the global state of a unit, so that it can be referred to in subprogram specifications. For example, a unit describing an HTML page might have a global variable to hold the content, and another one to hold the CSS style sheet:

package HTML_Page with
  Abstract_State => (Content, Style_Sheet)
is ...

Then, operations over this HTML page can specify whether they read or write the global state of the page.

  procedure Initialize_Content with
     Global => (Output => Content);

   procedure Update_Content (New_Item : Item) with
     Global => (In_Out => Content);

   procedure Display_Text with
     Global => (Input => (Content, Style_Sheet));

The above states that:

  • Initialize_Content should initialize the value of the Content global state, but not read it, and neither read not write the value of the Style_Sheet global state.
  • Update_Content may update the value of the Content global state, but neither read nor write the value of the Style_Sheet global state.
  • Similarly, Display_Text may read both parts of the global state, but it should not write any.

The benefit of describing global state abstractly thus appears already at the level of the unit spec, as a way to clearly describe interactions between subprograms and global state.

But the real benefit appears when checking that the body of the unit correctly implements its spec. First, each abstract state is refined into a list of concrete variables:

package body HTML_Page with
  Refined_State => (Content     => (Header, Content_Body, Footer),
                    Style_Sheet => (Background, Fonts, Title_Styles))
is
   Header       : HTML_Section;
   Content_Body : HTML_Section;
   Footer       : HTML_Section;
   Background   : Color;
   Fonts        : List_Of_Fonts;
   Title_Styles : List_Of_Styles;
   ...

Then, each Global contract of subprogram is expressed with respect to concrete variables, in a Refined_Global contract:

procedure Initialize_Content with
     Refined_Global => (Output => (Header, Content_Body, Footer)) is
   ...

   procedure Update_Content (New_Item : Item) with
     Refined_Global => (In_Out => Content_Body) is
   ...

   procedure Display_Text with
     Refined_Global => (Input => (Content_Body, Fonts, Title_Styles)) is
   ...

When the tool GNATprove is applied to this program, it checks that the refined contracts correctly refine the abstract ones (this is the case above), and that the implementation implements the refined contracts. For example, if Update_Content reads Header, contrary to what is specified in its Refined_Global contract, GNATprove issues an error:

html_page.ads:8:14: "Header" must be listed in the Refined_Global aspect of "Update_Content"

Or if Display_Text does not read the value of Fonts, contrary to what is specified in its Refined_Global contract, GNATprove issues a warning:

html_page.adb:26:49: warning: unused initial value of "Fonts" [unused_initial_value]

And that's not all! Thanks to contracts on subprograms, GNATprove can detect any possible read of uninitialized global variables. For example, if Initialize_Content attempts to read the value of Header before initializing it, GNATprove issues an error:

html_page.adb:22:20: "Header" is not initialized [uninitialized]

The same is true for client units of HTML_Page, which may also read and write its global state through calls to its API. If a client program calls Update_Content before Initialize_Content, GNATprove issues the error:

client.adb:8:04: "Content" is not initialized [uninitialized]

Finally, a special contract Initializes can be used to specify that a package initializes some state at elaboration, for example:

package HTML_Page with
  Abstract_State => (Content, Style_Sheet),
  Initializes    => Content
is

Again, GNATprove will check correct initialization of the concrete variable which refine global state Content here.

In summary, SPARK 2014 allows users to specify correct access to global variables, and the associated tool GNATprove checks that all accesses to global variables are indeed according to the specification

Posted in #Language    #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.