SPARK 18 Release Notes¶
We present here a few highlights of the new features in SPARK 18. You can access the complete list here.
Preconditions have been added to functions from the standard numerical package
Ada.Numerics.Generic_Elementary_Functions, in cases that may lead to
Constraint_Error when called on
actual parameters that are not suitable, like a negative input for
Sqrt. This ensures that GNATprove generates corresponding precondition
checks when such functions are called. For example, here are the preconditions on
function Sqrt (X : Float_Type'Base) return Float_Type'Base with Pre => X >= 0.0, ... function Log (X : Float_Type'Base) return Float_Type'Base with Pre => X > 0.0, ...
The formal containers library, which provides SPARK-compatible versions of Ada
containers, has been enriched with comprehensive contracts. These contracts use
functional, mathematical-like containers as models of imperative
containers. For example, here is the contract of function
expresses that the value returned is the value found in the functional model of
the list (which is a sequence) at the index corresponding to the cursor
Position obtained from the functional model of cursor positions (which is a
function Element (Container : List; Position : Cursor) return Element_Type with Global => null, Pre => Has_Element (Container, Position), Post => Element'Result = Element (Model (Container), P.Get (Positions (Container), Position));
These precise contracts can now be used to express more easily rich functional properties on programs that manipulate formal containers. For more details, see the description of the formal containers library in the SPARK User’s Guide. The loop examples in the SPARK User’s Guide have been updated to use these new specification capabilities.
It is now possible to specify that a subprogram is always terminating, for every value of its inputs allowed in its precondition. This in turns allows for easier proof of its callers in some cases. This is specified as follows:
function F (X : Natural) return Natural; pragma Annotate (GNATprove, Terminating, F);
GNATprove checks that property during flow analysis and emits a message if it cannot guarantee termination. See the SPARK User’s Guide for more details.
The engine of static analyzer CodePeer was integrated in SPARK Pro 17 to prove run-time checks and assertions in addition to the other distributed provers Alt-Ergo, CVC4 and Z3. The initial integration did not allow to benefit from the full capability of CodePeer. In particular, assertions (including pragma Assert and loop invariants) and checks on possible division by zero that were proved by CodePeer needed to be reproved by other provers in GNATprove. Additionally, the integration was not working in various scenarios, depending on the specific options selected or the particular project file configuration.
All these problems in the integration of CodePeer have been fixed, which allows
to fully benefit from the use of static analysis in GNATprove. CodePeer is
activated by using the switch
--codepeer=on on the command line, or by
selecting the checkbox CodePeer Static Analysis in the proof dialog
opened in GPS after selecting the ,
and similar menu entries.
In general, proving properties of code with loops requires writing loop invariants. This is not necessary anymore when the loop is simple enough, which entails in particular that it contains fewer than 20 iterations, and it does not come with a loop invariant already. See the SPARK User’s Guide for a precise definition of simple loops.
GNATprove now unrolls automatically simple loops. So a loop over 10 elements in an array A such as:
for J in Index loop A (J) := J; end loop;
is analyzed by GNATprove as if it was written without loop:
A (1) := 1; A (2) := 2; A (3) := 3; A (4) := 4; A (5) := 5; A (6) := 6; A (7) := 7; A (8) := 8; A (9) := 9; A (10) := 10;
In cases where a user does not want a loop to be unrolled this way, she can either:
add a dummy loop invariant
pragma Loop_Invariant (True);in the loop; or
call GNATprove with the switch
See also the blog post on Proving Loops Without Loop Invariants.
Some checks involving floating-point computations are particularly difficult to prove automatically, in particular when they don’t depend simply on computing coarse static bounds for the result of computations. This is related to the weaker support for floating-point arithmetic in provers, compared to the support of integer arithmetic.
We introduced a library of lemmas in SPARK Pro 17, that can be used to prove more complex properties that cannot be proved fully automatically, with manageable complexity for the user. We have now added lemmas about the monotonicity of floating-point operators. Thus, to prove that X * Z is less than Y * Z when X is known to be less than Y and Z is non-negative, all of them being floating-point variables, one can simply call the corresponding ghost procedure from the SPARK lemma library:
SPARK.Float_Arithmetic_Lemmas.Lemma_Mul_Is_Monotonic (X, Y, Z); -- here X * Z <= Y * Z is known
GNATprove will verify the conditions for using the lemma as specified in its
precondition. In the case above, these include
X <= Y and
See the SPARK User’s Guide for more details.
GNATprove more precisely tracks the dynamic type of tagged types (types used for Object Oriented programming in SPARK), both for variables and function results whose actual type is known statically. This translates in more precise proof of dispatching calls on such variables, as GNATprove can use the more precise contract when the controlling type of the dispatching call is known.
The use of manual proof allows to address more complex properties than cannot be proved fully automatically, with manageable complexity for the user, represented by the manual proof label in the following diagram:
With manual proof, the user can interactively manipulate the proof context for proving a property. With transformations (so-called tactics in the scientific literature on interactive proof), the user can modify the proof context to make it easier to solve by provers or to complete the proof manually. The following interface for manual proof is started by selecting the contextual menuon an unproved check message inside GPS:
As much as possible, the names of logic elements in the proof context follow the naming of variables from the program. When the proof is complete, the actions of the user are saved in the proof session file, which can be stored and shared under version control.
Private types whose full view is not in SPARK are now translated into clones of
__private Why3 abstract type, with unique names in
Why3. This allows to more easily map them to distinct existing logic types in
The precise list of Verification Conditions that were generated by GNATprove,
and which provers were called on each one, is now output by GNATprove in a
machine-parsable format in the
.spark files that are produced for every
analyzed unit. The content of these files is documented in the SPARK User’s
For an example of use of this data, see this blog post on third-party tools that compute statistics on GNATprove analysis results.
Users can get CWE ids in messages by using the new switch
--cwe. For example,
on a possible division by zero, GNATprove will issue a message including CWE 369:
file.adb:12:37: medium: divide by zero might fail [CWE 369]
This allows for easier analysis of messages based on the underlying vulnerabilities, for use in a security context.
For more information on CWE, see the MITRE Corporation’s Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program (http://cwe.mitre.org/).
Until SPARK Pro 17, extra setup was required to make GNATprove work with a
non-default runtime, even when the project file contained all the
information. Now, GNATprove uses the same mechanism to find the runtimes for
formal verification as GPRbuild does for compilation: as long as all required
tools are installed and on the PATH, SPARK will find and use the correct
runtime according to the
--target switches passed to it, or
Target attributes defined in the project.
The SPARK tools now support caching large parts of the analysis via a memcached
server. If a memcached server is available to store analysis results, and this
server is specified to GNATprove via the command line option
--memcached-server=hostname:portnumber, then subsequent invocations of the
tools, even across different machines, can store intermediate results of the
tools. The user-visible effect is that GNATprove can produce results faster.
See this blog post for more details.