Implementation Defined Aspects and Pragmas

This appendix lists all the aspects or pragmas specific to GNATprove.

Aspect and Pragma SPARK_Mode

SPARK_Mode is a three-valued aspect. At least until we get to the next paragraph, a SPARK_Mode of On, Off, or Auto is associated with each Ada construct. Roughly, the meaning of the three values is the following:

  • a value of On means that the construct is required to be in SPARK, and the construct will be analyzed by GNATprove.

  • a value of Off means that the construct will not be analyzed by GNATprove, and does not need to obey the SPARK restrictions. The construct also cannot be referenced from other parts that are required to be in SPARK.

  • a value of Auto means that the construct will not be analyzed, and GNATprove will infer whether this construct can be used in other SPARK parts or not.

As generic units are not directly analyzed by GNATprove, but only generic instances are, the meaning of the three values is slightly different for generic units:

  • a value of On means that instances can be in SPARK, depending on the parameters passed for the instantiation.

  • a value of Off means that instances cannot be in SPARK, independent of the parameters passed for the instantiation.

  • a value of Auto provides no information on whether instances can be in SPARK or not.

We now explain in more detail how the SPARK_Mode pragma works.

Some Ada constructs are said to have more than one “section”. For example, a declaration which requires a completion will have (at least) two sections: the initial declaration and the completion. The SPARK_Modes of the different sections of one entity may differ. In other words, SPARK_Mode is not an aspect of an entity but rather of a section of an entity.

For example, if a subprogram declaration has a SPARK_Mode of On while its body has a SPARK_Mode of Off, then an error would be generated if the subprogram took a parameter of a general access type but not if the subprogram declared a local variable of a general access type (recall that general access types are not in SPARK).

A package is defined to have 4 sections: its visible part, its private part, its body declarations, and its body statements. A protected or task unit has 3 sections: its visible part, its private part, and its body. Other declarations which require a completion have two sections, as noted above; all other entities and constructs have only one section.

If the SPARK_Mode of a section of an entity is Off, then the SPARK_Mode of a later section of that entity shall not be On. [For example, a subprogram can have a SPARK declaration and a non-SPARK body, but not vice versa.]

If the SPARK_Mode of a section of an entity is Auto, then the SPARK_Mode of a later section of that entity shall not be On, and it shall not be Off unless that entity is a generic entity, or an instance of such a generic. [This makes it possible to mark a later section of a generic unit as Off, in cases where its initial section is Auto to allow instantiations to have any value of SPARK_Mode.]

The SPARK_Mode aspect can be specified either via a pragma or via an aspect_specification. In some contexts, only a pragma can be used because of syntactic limitations. In those contexts where an aspect_specification can be used, it has the same effect as a corresponding pragma.

The form of a pragma SPARK_Mode is as follows:

pragma SPARK_Mode [ (On | Off) ]

The form for the aspect_definition of a SPARK_Mode aspect_specification is as follows:

[ On | Off ]

For example:

package P
   with SPARK_Mode => On
is

The pragma can be used as a configuration pragma. The effect of such a configuration pragma is described below in the rules for determining the SPARK_Mode aspect value for an arbitrary section of an arbitrary Ada entity or construct.

Pragma SPARK_Mode shall be used as a local pragma in only the following contexts and has the described semantics:

Pragma placement

Affected construct

Alternative aspect form

Start of the visible declarations (preceded only by other pragmas) of a package declaration

Visible part of the package

As part of the package_specification

Start of the visible declarations (preceded only by other pragmas) of a task or protected unit

Visible part of the unit

As part of the declaration

Start of the private declarations of a package, a protected unit, or a task unit (only other pragmas can appear between the private keyword and the SPARK_Mode pragma)

Private part

None

Immediately at the start of the declarations of a package body (preceded only by other pragmas)

Body declarations of the package

As part of the package_body

Start of the elaboration statements of a package body (only other pragmas can appear between the begin keyword and the SPARK_Mode pragma)

Body statements of the package

None

Start of the declarations of a protected or task body (preceded only by other pragmas)

Body

As part of the protected or task body

After a subprogram declaration (with only other pragmas intervening). [This does not include the case of a subprogram whose initial declaration is via a subprogram_body_stub. Such a subprogram has only one section because a subunit is not a completion.]

Subprogram’s specification

As part of the subprogram_declaration

Start of the declarations of a subprogram body (preceded only by other pragmas)

Subprogram’s body

As part of the subprogram_body

A default argument of On is assumed for any SPARK_Mode pragma or aspect_specification for which no argument is explicitly specified.

A SPARK_Mode of Auto can only be explicitly specified for a configuration pragma; the cases in which a SPARK_Mode of Auto is implicitly specified are described below. Roughly speaking, Auto indicates that it is left up to the formal verification tools to determine whether or not a given construct is in SPARK.

A SPARK_Mode pragma or aspect specification shall only apply to a (section of a) package, generic package, subprogram, or generic subprogram.

A SPARK_Mode of On shall only apply to a (section of a) library-level entity, except for the case of SPARK_Mode specifications occurring within generic instances. A SPARK_Mode of On applying to a non-library-level entity within a generic instance has no effect.

The SPARK_Mode aspect value of an arbitrary section of an arbitrary Ada entity or construct is then defined to be the following value (except if this yields a result of Auto for a non-package; see below):

  • If SPARK_Mode has been specified for the given section of the given entity or construct, then the specified value;

  • else for the instance of a generic unit, follow the rules as for a declaration that would not be a generic instantiation; take the resulting value of SPARK_Mode if it is Auto or Off; otherwise, take the value of SPARK_Mode specified for the generic unit if any; otherwise the value is On.

  • else for the private part of a public child unit whose parent unit’s private part has a SPARK_Mode of Off, the SPARK_Mode is Off;

  • else for the private part of a package or a protected or task unit, the SPARK_Mode of the visible part;

  • else for a package body’s statements, the SPARK_Mode of the package body’s declarations;

  • else for the first section (in the case of a package, the visible part) of a public child unit, the SPARK_Mode of the visible part of the parent unit;

  • else for the first section (in the case of a package, the visible part) of a private child unit, the SPARK_Mode of the private part of the parent unit;

  • else for any of the visible part or body declarations of a library unit package or either section of a library unit subprogram, if there is an applicable SPARK_Mode configuration pragma then the value specified by the pragma; if no such configuration pragma applies, then an implicit specification of Auto is assumed;

  • else the SPARK_Mode of the enclosing section of the nearest enclosing package or subprogram;

  • Corner case: the SPARK_Mode of the visible declarations of the limited view of a package is always Auto.

If the above computation yields a result of Auto for any construct other than one of the four sections of a package, then a result of On or Off is determined instead based on the legality (with respect to the rules of SPARK) of the construct. The construct’s SPARK_Mode is On if and only if the construct is in SPARK. [A SPARK_Mode of Auto is therefore only possible for (sections of) a package.]

In code where SPARK_Mode is On (also called “SPARK code”), the rules of SPARK are enforced. In particular, such code shall not reference non-SPARK entities, although such code may reference a SPARK declaration with one or more non-SPARK subsequent sections (e.g., a package whose visible part has a SPARK_Mode of On but whose private part has a SPARK_Mode of Off; a package whose visible part has a SPARK_Mode of Auto may also be referenced).

Code where SPARK_Mode is Off shall not enclose code where Spark_Mode is On. However, if an instance of a generic unit is enclosed by code where SPARK_Mode is Off and if any SPARK_Mode specifications occur within the generic unit, then the corresponding SPARK_Mode specifications occurring within the instance have no semantic effect. [In particular, such an ignored SPARK_Mode specification could not violate the preceding “Off shall not enclose On” rule because the SPARK_Mode of the entire instance is Off. Similarly, such an ignored SPARK_Mode specification could not violate the preceding rule that a SPARK_Mode specification shall only apply to a (section of a) library-level entity.]

For purposes of the “Off shall not enclose On” rule just described, the initial section of a child unit is considered to occur immediately within either the visible part (for a public child unit) or the private part (for a private child unit) of the parent unit. In addition, the private part of a public child package is considered to occur immediately within the private part of the parent unit. [This follows Ada’s visibility rules for child units. This means, for example, that if a parent unit’s private part has a SPARK_Mode of Off, then the private part of a public child package shall not have a SPARK_Node of On. Note also that a SPARK_Mode configuration pragma which applies only to the specification (not the body) of a child unit is always ineffective; this is a consequence of the rules given above for determining the SPARK_Mode of the first section of a child unit.]

The rules for a protected unit follow from the rules given for other constructs after notionally rewriting the protected unit as a package.

A protected unit declaration such as

protected type Prot
  with SPARK_Mode => On
is
   procedure Op1 (X : in out Integer);
   procedure Op2;
   function Non_SPARK_Profile (X : in out Integer) return Boolean
     with SPARK_Mode => Off;
private
   Aaa, Bbb : Integer := 0;
end Prot;

can be thought of, for purposes of SPARK_Mode rules, as being a lot like

package Pkg
  with SPARK_Mode => On
is
   type Prot is limited private;
   procedure Op1 (Obj : in out Prot; X : in out Integer);
   procedure Op2 (Obj : in out Prot);
   function Non_SPARK_Profile (Obj : Prot; Ptr : in out Integer) return Boolean
     with SPARK_Mode => Off;
private
   type Prot is
     limited record
        Aaa, Bbb : Integer := 0;
     end record;
end Pkg;

which is legal. The point is that a protected type which is in SPARK can have protected operation whose declaration is not in SPARK.

SPARK_Mode is an implementation-defined Ada aspect; it is not (strictly speaking) part of the SPARK language. It is used to notionally transform programs which would otherwise not be in SPARK so that they can be viewed (at least in part) as SPARK programs.

Note that if you would like to mark all your code in SPARK_Mode, the simplest solution is to specify in your project file:

package Builder is
   for Global_Configuration_Pragmas use "spark.adc";
end Builder;

and provide a file spark.adc which contains:

pragma SPARK_Mode;

Aspect and Pragma Iterable

In SPARK, it is possible to allow quantification over any container type using the Iterable aspect. This aspect provides the primitives of a container type that will be used to iterate over its content. For example, if we write:

type Container is private with
  Iterable => (First       => First,
               Next        => Next,
               Has_Element => Has_Element);

where

function First (S : Set) return Cursor;
function Has_Element (S : Set; C : Cursor) return Boolean;
function Next (S : Set; C : Cursor) return Cursor;

then quantification over containers can be done using the type Cursor. For example, we could state:

(for all C in S => P (Element (S, C)))

to say that S only contains elements for which a property P holds. For execution, this expression is translated as a loop using the provided First, Has_Element, and Next primitives. For proof, it is translated as a logic quantification over every element of type Cursor. To restrict the property to cursors that are actually valid in the container, the provided function Has_Element is used. For example, the property stated above becomes:

(for all C : Cursor => (if Has_Element (S, C) then P (Element (S, C))))

Like for the standard Ada iteration mechanism, it is possible to allow quantification directly over the elements of the container by providing in addition an Element primitive to the Iterable aspect. For example, if we write:

type Container is private with
  Iterable => (First       => First,
               Next        => Next,
               Has_Element => Has_Element
               Element     => Element);

where

function Element (S : Set; C : Cursor) return Element_Type;

then quantification over containers can be done directly on its elements. For example, we could rewrite the above property into:

(for all E of S => P (E))

For execution, quantification over elements of a container is translated as a loop over its cursors. In the same way, for proof, quantification over elements of a container is no more than syntactic sugar for quantification over its cursors. For example, the above property is translated using quantification over cursors :

(for all C : Cursor => (if Has_Element (S, C) then P (Element (S, C))))

Depending on the application, this translation may be too low-level and introduce an unnecessary burden on the automatic provers. As an example, let us consider a package for functional sets:

package Sets with SPARK_Mode is

  type Cursor is private;
  type Set (<>) is private with
    Iterable => (First       => First,
                 Next        => Next,
                 Has_Element => Has_Element,
                 Element     => Element);

  function Mem (S : Set; E : Element_Type) return Boolean with
    Post => Mem'Result = (for some F of S => F = E);

  function Intersection (S1, S2 : Set) return Set with
    Post => (for all E of Intersection'Result => Mem (S1, E) and Mem (S2, E))
      and (for all E of S1 =>
               (if Mem (S2, E) then Mem (Intersection'Result, E)));

Sets contain elements of type Element_Type. The most basic operation on sets is membership test, here provided by the Mem subprogram. Every other operation, such as intersection here, is then specified in terms of members. Iteration primitives First, Next, Has_Element, and Element, that take elements of a private type Cursor as an argument, are only provided for the sake of quantification.

Following the scheme described previously, the postcondition of Intersection is translated for proof as:

(for all C : Cursor =>
    (if Has_Element (Intersection'Result, C) then
           Mem (S1, Element (Intersection'Result, C))
       and Mem (S2, Element (Intersection'Result, C))))
and
(for all C1 : Cursor =>
    (if Has_Element (S1, C1) then
           (if Mem (S2, Element (S1, C1)) then
                 Mem (Intersection'Result, Element (S1, C1)))))

Using the postcondition of Mem, this can be refined further into:

(for all C : Cursor =>
    (if Has_Element (Intersection'Result, C) then
           (for some C1 : Cursor =>
               Has_Element (S1, C1) and Element (Intersection'Result, C) = Element (S1, C1))
       and (for some C2 : Cursor =>
               Has_Element (S2, C2) and Element (Intersection'Result, C) = Element (S2, C2))))
and
(for all C1 : Cursor =>
    (if Has_Element (S1, C1) then
           (if (for some C2 : Cursor =>
               Has_Element (S2, C2) and Element (S1, C1) = Element (S2, C2)))
    then (for some C : Cursor => Has_Element (Intersection'Result, C)
             and Element (Intersection'Result, C) = Element (S1, C1))))