Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property over such containers often involves quantifying over the elements they contain.

As seen in a previous post, in SPARK 2014, it is possible to allow quantification over any such container type using an 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:

where

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

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:

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:

where

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

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 :

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:

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:

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

Though perfectly valid, this translation may produce complicated proofs, especially when verifying complex properties over sets. For SPARK formalization of the new ada-trait-based containers, we introduced a new GNATprove annotation, that can be used to change the way for ... of quantification is translated. It can be used to provide GNATprove with a "Contains" function, that will be used for quantification. For example, on our sets, we could write:

With this annotation, the postcondition of Intersection is translated in a simpler way, using logic quantification directly over elements:

Note that care should be taken to provide an appropriate function contains, which returns true if and only if the element E is present in S. This assumption will not be verified by GNATprove.

The annotation Iterable_For_Proof can also be used in another case. Operations over complex data structures are sometimes specified using operations over a simpler model type. In this case, it may be more appropriate to translate for ... of quantification as quantification over the model's cursors. As an example, let us consider a package of linked lists that is specified using a sequence that allows accessing the element stored at each position:

Elements of lists can only be accessed through cursors. To specify easily the effects of position-based operations such as Append, we introduce a ghost type Sequence of unbounded arrays indexed by positive integers that is used to represent logically the content of the linked list in specifications. The sequence associated to a list can be constructed using the Model function. Following the usual translation scheme for quantified expressions, the last line of the postcondition of Init is translated for proof as:

Using the definition of Element and Has_Element, it can then be refined further into:

To be able to link this property with other properties specified directly on models, like the postcondition of Append, it needs to be lifted to iterate over positions instead of cursors. This can be done using the postcondition of Model that states that there is a valid cursor in L for each position of of its model. This lifting requires a lot of quantifier reasoning from the prover, thus making proofs more difficult.

The GNATprove Iterable_For_Proof annotation can be used to provide GNATprove with a "Model" function, that will be called to translate quantification on complex containers toward quantification on their model. For example, on our lists, we could write:

With this annotation, the postcondition of Init is translated directly as a quantification on the elements of the result's model:

Like with the previous annotation, care should be taken to define the model function such that it always return a model containing exactly the same elements as L.

On the formal version of ada-trait-based containers, tuning the way quantification is translated for proof is really important. Indeed, their specification is container intensive, as up to three different functional containers are used as models of imperative containers, and also quite complex as it must allow reasoning efficiently on containers at different levels. As an example, a "Contains" Iterable_For_Proof annotation is used to avoid introducing a parasitic type of cursors in the functional model of imperative sets. It is combined with a "Model" annotation on imperative set so that quantification on elements of a set are translated directly as a high level, content based, property on functional sets rather than as a low level, cursor aware quantification. As a result, if S in an imperative set, the property:

is translated for proof as:

which both makes the work of provers easier and allows a clean separation between low-level, cursor aware properties and high-level, content based specifications.