Rationale of SPARK

• Major Considerations in the Design of SPARK
SPARK was designed for use in high integrity applications; it is therefore essential that it exhibits logical soundness, simplicity of the formal definition, expressive power, security, verifiability, bounded space and time requirements, and minimal runtime system requirements.

• SPARK Language Features
SPARK is a subset of the Ada language. It includes Ada constructs regarded as essential for the construction of complex software, such as packages, private types, typed constants, functions with structured values, and the library system. It excludes tasks, exceptions, generic units, access types, use clauses, type aliasing, anonymous types, default values in record declarations, default subprogram parameters, goto statements, and declare statements.

• Mandatory Annotations
The requirements for analysis and verification imply a need for (non-Ada) formal comments which supply extra information to the SPARK tools. These annotations include:
• global definitions in procedures (which declare 'imported' or 'exported' global variables) or functions (which import such variables);
• dependency relations in procedures (which specify the imported variables which are required to derive the value of each exported variable);
• the inherit clause in a SPARK package declaration (which restricts penetration of the package to items specifically imported from other packages);
• the own variable clause in a SPARK package specification (which makes actions on the package state visible to analysis tools);
• the initialisation annotation in a SPARK package specification (which indicates the initialisation by the package of its own state).

• 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.

• Tool Support
The SPARK Examiner checks conformance to the rules of SPARK and the consistency between SPARK code and annotations. It can also generate verification conditions and (together with the SPADE proof-checker) provide support for the formal proof of SPARK programs.


Designing with SPARK

• Design by Decomposition and Abstraction
Decomposition (ie the partitioning of a problem into simpler components) and abstraction (ie the choice of an appropriate level of detail) are powerful tools in program design. Abstraction helps in making a good choice of program components which are easy to specify, build and combine.

• Language Support for Decomposition
• A SPARK program is composed of one or more program units; each unit is either a subprogram or a package.
• A subprogram expresses a sequence of actions and is either a procedure (which updates state) or a function (which views the state). SPARK annotations (eg global definitions and dependency relations) make explicit the data transactions between a subprogram and its calling environment and thus overcome language insecurities such as the risk of aliasing.
• A package is a collection of data types, data objects and subprograms.
• A SPARK program unit in general consists of a specification and a body. The specification is the interface between the unit and the rest of the program; the body is the actual implementation of the unit and can be hidden from its users.
• The specification and body of a unit may be written and compiled separately. Program units are integrated by means of a program library.

• Language Support for Abstraction
Abstraction by parameterisation can be implemented by the use of procedures. Abstraction by specification can be implemented by:
• the abstract data type, which consists of a specification for a set of objects and a set of operations that characterise the behaviour of those objects;
• the abstract state machine, which is an abstract data type with internal state.

• SPARK Abstract Data Types
An abstract data type may be constructed in SPARK from a package containing private types. A package consists of a specification and a body. The package specification defines the interface between the package and the rest of the program and (by use of the appropriate SPARK annotations) may have a visible part and a private part. The visible part declares entities that may be used outside the package and the private part declares entities which may be used within the package but not outside it.

• SPARK Abstract State Machines
• An abstract state machine may be constructed in SPARK from a package with variables (to record the state of the machine) declared in its body. The own annotation makes the state variable(s) visible for specification and analysis purposes.
• The procedures which act on the machine and the functions which observe its state are specified in the visible part of the package specification; all other details are hidden in the package body.
• Initialisation of the state is implemented by means of a statement part in the package body, together with an initializes annotation.

• Refinement
• Until the package body of an abstract state machine has been designed in detail, it may be difficult to determine how the state should be represented. Furthermore, even if the specification to this level of detail could be achieved at an early stage, the dependency relations would be unnecessarily complex. The method of refinement overcomes these difficulties.
• Refinement involves the progressive replacement of an abstract state description by less abstract versions. It provides a controlled way of moving from an abstract specification to an implementation.
• In SPARK, refinement is performed (once the package body has been written) by the use of refinement clauses. These clauses relate each abstract state variable to the state variables (known as the "constituents" of the abstract state variable) which are used in the actual implementation of the package body.


Formal Semantics of SPARK

• Reasons for a Formal Definition
A formal mathematical definition of the SPARK language was produced in order to:
• provide a sound basis for systematic refinement and implementation in SPARK of "model-based" formal specification languages such as Z and VDM;
• justify certain procedures employed within the SPARK Examiner, such as those of the Run-Time Error Checker.

• Structure of Formal Definition
The formal definition of SPARK is presented in two parts; the static semantics (eg the rules for the detection of aliasing in SPARK programs) and the dynamic semantics (eg the effect each executable SPARK statement has on the program environment).

• Content of Formal Definition
• The formal definition is written in the Z formal notation (extended with notation for inference rules) as a structured operational semantics. An operational semantics describes the evaluation of SPARK programs on an abstract machine; transitions in the state of this machine are defined for each stage of the evaluation.
• The main component of each state of the machine is a term in the abstract syntax of SPARK and thus the structure of the definition of SPARK follows from the structure of the SPARK language itself.
• In order to define the meaning of SPARK statements, the state of the abstract machine includes the environment (which contains the types of variables and the definitions of procedures), the store (which contains the values of the variables) and a term from the abstract syntax of SPARK. Each transition of the abstract machine is defined by a rewrite rule.