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

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

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

  1. A name denoting the abstract view of an object shall occur only:

    1. as a global_item in a Global or Refined_Global aspect specification; or

    2. as an input or output in a Depends or Refined_Depends aspect specification; or

    3. in an input_list of an Initializes aspect.

Static Semantics

  1. 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.]

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