The SPARK Examiner

Standard Program Analysis

The Examiner checks conformance of a SPARK source text to the rules of SPARK by performing the following analyses.

• Lexical and Syntactic Analysis
The Examiner first carries out lexical and syntactic analysis of each compilation unit. In addition to checking for syntactic correctness, this analysis also permits the Examiner to identify which other units are required in order to carry out the complete analysis of each unit. These other units are then read by the Examiner.

• Static Semantic Analysis
The Examiner then checks that the given compilation units satisfy the static-semantic rules of SPARK. This analysis checks for items such as aliasing and elaboration order dependencies.

• Control Flow Analysis
This analysis checks that the placement of exit and return statements conforms to the rules of SPARK, thus guaranteeing that SPARK programs are well-structured.

• Data and Information Flow Analysis
The Examiner performs data and information flow analysis in order to check for:

• references to uninitialised data
• ineffective statements
• inconsistencies between the expected and actual information flow
• loop stability
• variables declared but not used
• variables whose value will not change.

Run-Time Error Checking

Compliance with the rules of SPARK (as checked by standard program analysis) does provide protection against many common programming errors such as failure to initialise variables, and also against more obscure defects such as aliasing of procedure parameters. However, there is an important class of errors against which protection is not immediately provided – that of run-time errors. Run-time errors may be characterised as those which cannot be detected (or at least, not easily detected) at compilation time. In order to demonstrate that a SPARK program never gives rise to a run-time error, theorem proving is required.

• Run-Time Errors in SPARK Programs
Many of the run-time errors of Ada cannot occur in SPARK programs. However, the following run-time errors may still arise in SPARK programs:

• array index out of range
• type range violation
• division by zero
• numerical overflow

• Generating Proof Obligations
The formal definition of SPARK was used to specify the appropriate proof obligation for each run-time error. The proof obligation is a theorem which must be proved in order to show that the run-time error will never occur. The Run-Time Error Checker systematically generates the proof obligations for all possible run-time errors in a SPARK program.

• Automatic Proof
The Automatic Simplifier will discharge many of the generated proof obligations automatically. Any remaining undischarged obligations may be proved with the assistance of the SPADE Proof Checker.


Program Verification

• Overview
• The functional requirements of a SPARK subprogram can be expressed formally as a precondition (ie a predicate which expresses a constraint on the imported variables of the subprogram) and a postcondition (ie a predicate which expresses the relationship between the initial values of the imported variables and the final values of the exported variables of the subprogram).
• A program is said to be partially correct if, given that the precondition is satisfied on entry to the program and the program terminates, then the postcondition holds upon exit from the program. A program is said to be totally correct if it is partially correct and it always terminates. Note that even a totally correct program may still suffer from run-time errors and so a complete analysis of the program must also involve the use of the Run-Time Error Checker.
• The Examiner provides fully-automated support for the generation of proof obligations for partial correctness.

• Proof Contexts
In SPARK, preconditions and postconditions are expressed as annotations called proof contexts. These are special non-mandatory annotations which support the formal proof of SPARK programs. They are written in an expression language which is an extension of Ada's. Each proof context is associated with a particular location in the code:
• the precondition of a procedure or function is associated with the begin of its body: it specifies conditions under which the procedure or function should be called;
• the postcondition of a procedure (or the return annotation of a function) is associated with the end of the subprogram body: it defines the expected final state;
• each assert statement (eg a loop invariant) or check statement (ie a well-formation statement) is located between two executable statements: it specifies the state expected of the program at that point.

• The Origin of Proof Annotations
Ideally, the proof contexts should be derived from a formal mathematical specification. This derivation is not completely mechanical; apart from the inevitable differences between the specification and proof context notations, data types in the proof contexts must be expressed in concrete form (eg as arrays), rather than in the abstract form (eg sets or sequences) likely to be encountered in a formal specification.

• Generating Verification Conditions
A verification condition describes the requirements for correctness of the path between two cutpoints in a SPARK program (ie a precondition, postcondition or assert annotation). It is generated automatically by the Examiner from the assertions at the cutpoints and the SPARK program statements which lie along the path.

• Automatic Proof
The Automatic Simplifier will discharge many of the generated verification conditions automatically. Any remaining undischarged conditions may be proved with the assistance of the SPADE Proof Checker.

Analysis of Timing and Memory Usage

The SPARK language is designed to be statically analysable for both its worst-case execution time and memory usage. Constructs which may lead to unpredictable execution time (e.g. allocators) or memory use (e.g. recursion) are excluded from SPARK.

• Worst-Case Execution Time Analysis
The static analysis of program execution time requires analysis of program source text, object code, and user-supplied annotations. The latter supply information that cannot be determined automatically, such as a bound on the number of iterations made by each looping statement. By combining the control-flow graph for each subprogram, the program's call-tree, and the worst-case execution time for each object code fragment, the worst-case execution time (WCET) of a subprogram can be determined. Such analysis has several uses:
• Potential timing problems can be found earlier than usual, and thus can be corrected more cheaply and effectively.
• Watchdog timers can be set to monitor and control the execution of time-critical code.
• The program path that leads to WCET can be identified and tested with confidence.

• Worst-Case Stack Usage Analysis
In real-time and embedded systems, the accurate analysis of memory usage is crucial. Ideally, an engineer should be able to show that a program will never exceed its memory allocation through an entirely static analysis of program source text and/or object code. SPARK enables such analysis through excluding language features which may lead to unpredictable memory use either explicitly (e.g. allocators and access types) or implicitly (e.g. functions returning unconstrained types, and the "&" operator).
Ada programs typically allocate data in one of three areas:
• the stack,
• a fixed-size area for compile-time allocated data,
• a "heap" structure.

SPARK programs can be written which use no heap, and so the static analysis of memory usage in SPARK programs reduces to an analysis of worst-case stack usage.

Again, through an analysis of program source text, object code, and annotations, worst-case stack usage can be predicted.

• Tool Support
Several research groups have demonstrated static WCET and stack-usage tools, and commercial tool support is beginning to appear. A future release of the Examiner will include source-level annotations supporting static analysis of timing and stack usage. These will be processed by the Examiner into a form which is acceptable to third-party tools, initially the STAMP toolset from York Software Engineering Ltd.