10. Program Structure and Compilation Issues
SPARK supports constructive, modular analysis. This means that analysis may be
performed before a program is complete based on unit interfaces. For instance,
to analyze a subprogram which calls another all that is required is a
specification of the called subprogram including, at least, its
global_specification
and if formal verification of the calling program is to
be performed, then the Pre and Postcondition of the called subprogram need to
be provided. The body of the called subprogram does not need to be implemented
to analyze the caller. The body of the called subprogram is checked to be
conformant with its specification when its implementation code is available and
analyzed.
The separate compilation of Ada compilation_units
is consistent with
SPARK modular analysis except where noted in the following subsections but,
particularly with respect to incomplete programs, analysis does not involve the
execution of the program.
10.1. Separate Compilation
Legality Rules
A program unit cannot be a task unit, a protected unit or a protected entry.
10.1.1. Compilation Units - Library Units
No restrictions or extensions.
10.1.2. Context Clauses - With Clauses
Legality Rules
With clauses are always in SPARK, even if the unit mentioned is not completely in SPARK.
10.1.2.1. Abstract Views
State abstractions are visible in the limited view of packages in SPARK. The
notion of an abstract view of an object declaration is also introduced, and
the limited view of a package includes the abstract view of any objects
declared in the visible part of that package. The only allowed uses of an
abstract view of an object are where the use of a state abstraction would be
allowed (for example, in a Global aspect_specification
).
Legality Rules
A name denoting the abstract view of an object shall occur only:
as a
global_item
in a Global or Refined_Global aspect specification; oras an
input
oroutput
in a Depends or Refined_Depends aspect specification; orin an
input_list
of an Initializes aspect.
Static Semantics
Any state abstractions declared within a given package are present in the limited view of the package. [This means that, for example, a Global
aspect_specification
for a subprogram declared in a library unit package P1 could refer to a state abstraction declared in a package P2 if P1 has a limited with of P2.]For every object declared by an
object_declaration
occurring immediately within the visible part of a given package, the limited view of the package contains an abstract view of the object.
10.1.3. Subunits of Compilation Units
No restrictions or extensions.
10.1.4. The Compilation Process
The analysis process in SPARK is similar to the compilation process in Ada
except that the compilation_units
are analyzed, that is flow analysis and
formal verification is performed, rather than compiled.
10.1.5. Pragmas and Program Units
No restrictions or extensions.
10.1.6. Environment-Level Visibility Rules
No restrictions or extensions.
10.2. Program Execution
SPARK analyses do not involve program execution. However, SPARK programs are executable including those new language defined aspects and pragmas where they have dynamic semantics given.
10.2.1. Elaboration Control
No extensions or restrictions.