Abstraction is a key concept in programming as it can drastically simplify both implementation and code maintenance. It is particularly well suited to SPARK and its modular analysis. This section explains what state abstraction is and how it can be specified in SPARK. We will provide details on how it impacts GNATprove's analysis both in terms of information flow and proof of program properties.
State abstraction allows to:
- express data dependencies (
Globalcontract) and flow dependencies (
Dependscontract) that would not be expressible otherwise, as some data read/written is not visible at the point where the subprogram is declared;
- reduce the number of variables that need to be considered in flow analysis and proof, which may be critical for scaling the analysis to programs with thousands of global variables.
What is an Abstraction?¶
The abstraction principle is commonly used in programming languages. It consists in having two views of the same object: an abstract one and a refined one. The abstract one --- usually called specification --- only describes what the object does in a coarse way. A subprogram's specification usually explains how it should be called, how many parameters it has, of which type, etc., as well as what it will do, return a result, modify one of its parameters, etc.
Contract based programming as supported in Ada allows contracts to be added to a subprogram's specification. Contracts can be used to describe the subprogram's behavior in a more fine-grained manner. All the details of how the subprogram actually works are left to its refined view, that is, its implementation.
Take a look at the example code shown below:
The specification of the subprogram
Increase states that it should be
called on a unique argument, which should be a variable of type
Integer smaller than 100. Via this contract, it ensures that its
only effect will be to strictly increase the value of its argument.
Why is Abstraction Useful?¶
To obtain a good abstraction of a subprogram's implementation, its specification should summarize exactly what users of an object can rely on. In other words, user code should not rely on a behavior of an object's implementation if it is not documented in its specification.
For example, callers of the subprogram
Increase can assume that it
will always strictly increase the value of its argument. On our user code
snippet shown below, it means that the loop is bound to terminate.
They can also assume that the implementation of
Increase won't cause
any runtime error when called in the loop. However, on the other hand, the
assertion may fail if
Increase's implementation is changed.
If this basic principle is followed, abstraction can bring significant advantages. First, it simplifies both the program's implementation and its verification. Often, it is enough to understand the specification of an object to use it, which is in general simpler than trying to understand its actual implementation. It also makes maintenance and code reuse that much easier, as changes to the implementation of an object won't affect the code using this object.
GNATprove respects the abstraction defined by subprogram contracts, and as a
result does not prove the assertion after the loop in
Abstraction of a Package's State¶
Subprograms are not the only objects that can benefit from abstraction.
The state of a package --- that is, the set of persistent variables
defined in it --- can also be hidden from external users. This form of
abstraction --- called state abstraction --- is usually achieved by
defining variables in the body or private part of a package, so that they
can only be accessed through subprogram calls. For example, our
package shown below provides an abstraction for a unique
which can be modified using the
package Stack is procedure Pop (E : out Element); procedure Push (E : in Element); end Stack; package body Stack is Content : Element_Array (1 .. Max); Top : Natural; ... end Stack;
The fact that it is implemented using an array is irrelevant to the user and could be changed without impacting user code.
Declaring a State Abstraction¶
As the hidden state influences the program's behavior, SPARK allows it to
be declared. For this, a named state abstraction can be introduced using
Abstract_State aspect. This is not mandatory even for a package
which has hidden state. Several state abstractions can also be introduced
for the hidden state of a single package or for a package with no hidden
state at all. Note however that, as SPARK does not allow aliasing,
different state abstractions must always refer to disjoint sets of
concrete variables. Note also that a state abstraction is not a variable,
it does not have a type and cannot be used inside expressions, be it in
bodies or in contracts.
For example, we can optionally define a state abstraction for the whole hidden
state of the
Stack package like this:
package Stack with Abstract_State => The_Stack is ...
Alternatively, we can define a state abstraction for each hidden variable:
package Stack with Abstract_State => (Top_State, Content_State) is ...
Note that a state abstraction is not a variable (it has no type), and cannot be used inside expressions. For example:
pragma Assert (Stack.Top_State = ...); -- compilation error: Top_State is not a variable
Refining an Abstract State¶
Once an abstract state has been declared in a package, it must be refined into
its constituents using a
Refined_State aspect. The
aspect must be placed on the package's body even if the package previously did
not require a body before the addition of
Abstract_State. For each state
abstraction declared for the package, the refined state lists the set of
variables which are represented by this state abstraction.
If an abstract state is specified for a package, then it must be complete,
in the sense that every hidden variable must be part of a state
abstraction. For example, on our
Stack package's body, we must add a
Refined_State aspect linking the state abstraction
that we have introduced to the whole hidden state of the package,
Representing Private Variables¶
State abstractions are always refined in the package's body, where all the
variables are visible. When only the package's specification is available,
we need a way to specify to which state abstraction private variables
belong. This is done using the
Part_Of aspect on the variable's
Part_Of annotations are mandatory: if a package has an abstract
state annotation, then all the hidden states defined in its private part
must be linked to a state abstraction. For example:
If we choose to define
Stack's private part
instead of its body, then we must add a
Part_Of aspect to both
their declarations, associating them with the state abstraction
The_Stack, even though it is the only state abstraction defined in
Stack. Note that they still need to be listed in the
Refined_State aspect in the
package body Stack with Refined_State => (The_Stack => (Content, Top))
Until now, we have only seen hidden variables. But variables are not
the only constituents of a package's state. If a package
P contains a
nested package, then the nested package's state is part of
As a consequence, if the nested package is hidden, its state is part of
P's hidden state and must be listed in
P's state refinement.
This is the case in our example shown below, where the package
Hidden_Nested's hidden state is part of
P's hidden state:
Note that a visible state of
Hidden_Nested would also have been part
P's hidden state. Also note that, if
P contains a visible
nested package, then the nested package's state is not part of
hidden state. In particular, its hidden state should be declared in a
separate state abstraction on its own declaration, like it is done on our
Constants with Variable Inputs¶
Other possible constituents of a state abstraction are constants with variable inputs. We call constants with variable inputs constants whose value depends on either a variable or a subprogram parameter. Those are usually handled as variables in flow analysis, as they participate to the flow of information between variables throughout the program. Thus, constants with variable inputs, just like variables, are considered to be part of a package's state.
If a state abstraction is specified for a package, then hidden constants with variable inputs declared in this package must be listed in the state abstraction refinement. Note that, on the other hand, constants without variable inputs do not participate to the flow of information and therefore cannot appear in a state refinement.
Let's look at this example:
Max --- the maximal number of elements that can be stored in the
stack --- is initialized with a variable from an external package. Since
it now has variable inputs,
Max must be a part of the state
Global and Depends¶
As hidden variables can only be accessed through subprogram calls,
subprogram's contracts are the proper way of documenting how state
abstractions can be modified during the program's execution. First off,
Depends contracts can be used to specify which of
the state abstractions are accessed by a subprogram and how their values
flow through the different variables. Note that
Depends contracts referring to state abstractions may be less
precise than contracts referring to visible variables, as the different
modes of the hidden variables aggregated in a state abstraction are
collapsed into a single mode.
Depends contracts to the
in our stack:
In this example, the
Pop procedure only modifies the value of the
Top and keeps
Content unchanged. If two distinct
state abstractions are used for the two variables, then this contract is
Let's contrast this example with a different expression of
Depends contracts using a unique abstract state:
Content_State are collapsed into one single
state abstraction. In this case, we lose the fact that
preserved, only keeping the fact that
The_Stack is modified. This loss
in precision is reasonable here, it is the whole point of abstraction. But
users must be careful not to aggregate unrelated hidden state lest their
annotations become meaningless.
If imprecise contracts dealing with state abstractions as a whole are
perfectly reasonable for users of a package,
Depends contracts should remain as precise as possible inside the
package's body itself. For this reason, SPARK introduces the notion of
refined contracts. Those are precise contracts, specified on the bodies of
subprograms, where state refinements are visible. These contracts are
exactly like normal
Depends contracts, except
they refer directly to the hidden state of the package.
When a subprogram is called inside the package's body, these refined contracts
are used instead of the general ones, so that the verification can be as
precise as possible. Note that refined
optional: if they are not specified by the user, GNATprove will compute them to
check the package's implementation.
Stack example, we could add refined contracts like this:
Preconditions and Postconditions¶
Functional properties of subprograms are usually expressed using preconditions and postconditions. As these contracts are standard Boolean expressions, they cannot refer directly to state abstractions. To work around this restriction, functions can be defined to query the value of hidden variables. These functions can then be used in place of the state abstraction in other subprograms's contracts.
For example, we can query the state of the stack with functions
Is_Full, and call these in the contracts of procedures
Depends contracts, it is often useful to
have a more precise view of functional contracts when the hidden variables are
visible. This can be achieved using expression functions like we did for
Is_Full above. As expression function bodies act
as contracts for GNATprove, they automatically give a more precise version of
the contracts when their implementation is visible.
It may be the case that we need a more constraining contract to verify the
package's implementation than we want to ensure outside the abstraction. This
can be achieved using the
Refined_Post aspect. This aspect, when placed
on a subprogram's body, is used to provide stronger guaranties to internal
callers of a subprogram. If provided, the refined postcondition must imply the
subprogram's postcondition. This is checked by GNATprove, who will report a
failing postcondition if the refined postcondition is too weak, even if it is
actually implied by the subprogram's body. Note that SPARK does not supply a
similar notation for preconditions.
For example, we can refine the postconditions stated previously for procedures
Push, inside their respective refined postconditions:
Initialization of Local Variables¶
As part of flow analysis, GNATprove checks for proper initialization of variables. Therefore, flow analysis needs to know which are the variables initialized during the package's elaboration.
Initializes aspect can be used to specify the set of visible
variables and state abstractions of a package that are initialized during
its elaboration. Note that an
Initializes aspect cannot refer to a
variable that is not defined in the unit as, in SPARK, a package
shall only initialize variables declared immediately within the package.
Initializes aspects are optional. If they are not supplied by the
user, they will be computed by GNATprove.
Stack example, we could add an
Initializes aspect like
As flow analysis can also check for dependencies between variables, it
must be aware of information flowing through initialization of states. The
Initializes aspect also serves this purpose. If the initial value
of a variable or state abstraction is dependent on the value of a visible
variable or state abstraction from another package, then this dependency
must be listed in the
Initializes contract. The list of entities on
which a variable's initial value depends are associated to the variable
using an arrow.
Let's look at this example:
In our example, we stated in the
Initializes aspect of
V2's initial value depends on the value of
Note that we omitted the dependency for
V1, as its initial value does
not depend on any external variable. This dependency could also have been
stated explicitly, writing
V1 => null.
Dependencies of initial values can be computed by GNATprove if no
Initializes aspect is supplied. On the other hand, if an
Initializes aspect is provided for a package, then it should be
complete, that is, every initialized state of the package should be
listed, along with all its external dependencies.
Code Examples / Pitfalls¶
This section contains some code examples and pitfalls.
Communication defines a hidden
Ring_Buffer local package whose
capacity is initialized at elaboration from an external configuration.
This example is not correct. Here,
Capacity is declared in the private
Communication. Therefore, it should be linked to
declaration using the
Part_Of to the state of hidden local package
this time we hide variable
Capacity inside the private part of
This program is correct and GNATprove is able to verify it.
Counting defines two counters
Red_Counter, and provides separate initialization procedures for each, that
are called from the main procedure.
Although this program does not read uninitialized data, GNATprove fails to
verify this fact. As we have provided a state abstraction for package
Counting, flow analysis computes subprograms's effects in terms of this
state abstraction, and thus, will consider
State as an in-out global of
Reset_Red_Counter. Hence the message
issued by GNATprove requiring that
State be initialized after elaboration,
as well as the warning that no procedure in package
Counting can initialize
Let's remove the abstract state on package
This example is correct. Here, no state abstraction is provided. GNATprove will reason in terms of variables and will prove data initialization without any problem.
Let's restore the abstract state on package
Counting, but this time
providing a procedure
Reset_All calling the initialization procedures
This example is correct. Flow analysis computes refined versions of
Global contracts for internal calls which are used to verify that
Reset_All indeed properly initializes
State. Note that
Global annotations are not mandatory, they can
also be computed by GNATprove.
Let's consider yet another version of our abstract stack unit.
This example is not correct. There is a compilation error in
The_Stack is a state abstraction and not a
variable and cannot be mentioned in an expression.
In this version of our abstract stack unit, a model of the stack is returned by
Get_Stack, which can be called from the postcondition of
to specify that the stack should not be modified if it is full. Then, we can
Use_Stack that after pushing an element on the stack, either the
stack is unchanged (if the stack was full already) or its top element is equal
to the element just pushed.
This program is correct, but GNATprove cannot prove the
Use_Stack. Indeed, even if
Get_Stack is an expression
function, its body is not visible outside of
Stack's body where it is defined.
Let's move the definition of
Get_Stack and other expression functions
inside the private part of the spec of
This example is correct. GNATprove is able to verify the assertion in
Use_Stack since it has visibility over
Data defines three variables
that are initialized at elaboration (in
Data's package body) from an
external interface reading the file system.
This example is not correct. The dependency between
File_System must be listed in
Let's remove the
Initializes contract on package
This example is correct. Since
Data has no
GNATprove computes the set of variables initialized during its elaboration, as
well as their dependencies.