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