February 2016
34
T
ools
& S
oftware
cise the code with calls that violate precondi-
tions. After sufficient confidence is gained, the
contract checks can be disabled for efficiency,
but the contracts remain in the source code
as useful and unambiguous documentation
for whoever is reviewing or maintaining the
program. This approach can be used with
full Ada; there is no need to comply with the
SPARK subset.
Many constructs in Ada (and thus also in
SPARK) have implicit preconditions associ-
ated with them. For example an array index
has to be within the bounds of the array (thus
preventing buffer overrun), and the values of
the operands of an integer expression have to
be such that the operation will not overflow.
If these preconditions are violated then an
exception will be raised.The SPARK proof tool
will attempt to prove the implicit contracts. If
it succeeds then that guarantees that runtime
exceptions will not be raised. If any cannot be
proved then the programmer will be alerted
to the potential problem and can investigate
further; in some cases the proof tool may be
able to construct a counterexample showing
how the precondition will be violated.
Thus in an example such as the Min function,
although there is not enough information in
the function body to allow the postcondi-
tion to be proved (a loop invariant needs to
be specified), the SPARK proof tool can still
verify that the code cannot raise an excep-
tion. This is an important benefit. The func-
tional correctness of the program can then be
established with traditional testing methods
as described.
In a large application it may be appropriate to
apply formal methods to critical kernel code,
but unrealistic (perhaps because of the use of
full Ada or other languages) to use proof tech-
nology on modules that invoke the proved
code. In order to rely on the proof of the
kernel code, the developer of the unproved
code needs to ensure (by analysis, inspection,
or testing) that all variables that are used as
input by the proved code are initialized, and
also that the precondition of the proved code
is satisfied at each call. The postcondition of
the proved code can be assumed by the caller,
which may simplify the testing.
The need to call unproved code from proved
code can arise, for example, if a low-level rou-
tine in assembler or in a language not amena-
ble to proof technology is to be invoked from
a subprogram that will be formally analyzed.
An interface to the unproved code can be
specified in SPARK with the relevant con-
tracts. The developer of the unproved code
needs to ensure, through testing, that all data
flow dependency contracts are satisfied and
also that the postcondition for the unproved
code is met. The calling code will be analyzed
to make sure that the precondition for the
unproved code is satisfied at each call. The
techniques just described can be used when
an existing project is to be extended with
modules that will be subject to formal anal-
ysis. Furthermore, if the project is in Ada the
SPARK proof tool can automatically synthe-
size flow analysis contracts from the bodies
of the subprograms, thus providing a starting
point for formal verification (if the subpro-
gram is in the SPARK subset).
In a language with compile-time type check-
ing (such as Ada, C, and C++) detecting an
error such as an assignment of an integer to a
record (struct) does not require runtime test-
ing; defects of this kind are caught early and
inexpensively because the program will not
compile. Analogously, formal methods can
move runtime check failures and even logic
errors into the same detected before testing
starts category. Formal methods can thus
bring tangible benefits to the software verifi-
cation process, providing mathematics-based
assurance concerning program properties
that otherwise might only be demonstrated
with significant testing resources. Software
certification authorities have taken notice. For
example the DO-178C [7] standard for air-
borne software has an associated supplement
DO-333 [8] that shows how formal methods
may be used to automate some of the verifica-
tion activities and thereby reduce the certifica-
tion effort and cost.
A major impediment to the adoption of for-
mal methods in the past has been the apparent
need to commit to new development and ver-
ification processes. That is no longer the case.
As illustrated by the SPARK 2014 language
and proof technology, formal verification
and traditional testing methods are highly
compatible and complement each other in
a well-defined fashion. Contract-based pro-
gramming is in effect making the low-level
requirements part of the source program, and
with the Ada/SPARK approach the developer
can choose to verify them either statically or
dynamically based on project goals.
n
SPARK 2014
SPARK 2014 is an Ada 2012 subset that is amenable to proofs of program properties rang-
ing from absence of runtime errors to compliance with formally specified requirements. It
includes most of Ada data type facilities (numeric types, array types, record types, enumer-
ation types), code modularization (subprograms), generic templates, modules (packages),
encapsulation (private types), object-oriented programming, and a subset of Ada concur-
rency features (the Ravenscar profile).
SPARK excludes access types (pointers) and the goto statement, prohibits aliasing of assign-
able objects (where the same object is designated by different names), and ensures that all
expressions, including function calls, are free of side effects. These restrictions guarantee
deterministic behaviour (thus no implementation-dependent or implementation-defined
effects) and facilitate formal analysis. For example, an attempt to read the value of an unini-
tialized variable is not permitted in SPARK.
The SPARK subset is sufficiently expressive to implement critical applications, and earlier
versions of the language have been used in Air Traffic Management, aircraft avionics, smart
cards, and many other safety-critical and high-security systems. Further, ultra-high reliability
was achieved via a level of effort no greater than with traditional (testing-based) methods, in
part because errors were detected very early.
Formal analysis of SPARK programs is based on the inclusion of contracts in the source code.
SPARK uses the Ada 2012 syntax for contract-based programming, so any SPARK program
can be compiled by a standard Ada compiler.
SPARK contracts are used for two main purposes: flow analysis, and requirements on func-
tional behavior. Flow analysis contracts relate to data initialization and a subprogram depen-
dencies on global data, and also to the relationship between a subprogram inputs and its
outputs. A functional behavior contract is an assertion about the program state at a particular
point in execution. It is specified as a Boolean expression that can reference subprogram
parameters (both on entry and return), the subprogram result value (for a function), and
local and global data.
The SPARK proof tool will analyze a program, check that it complies with the SPARK lan-
guage restrictions, and attempt to prove the contracts that are explicitly supplied. It can also
synthesize flow analysis contracts (if not present) from subprogram bodies.
n
