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:

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

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:

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

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:

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:

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:

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:

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

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