12.12 Ada.Containers.Formal_Indefinite_Vectors (a-cfinve.ads)

This child of Ada.Containers defines a modified version of the Ada 2005 container for vectors of indefinite elements, meant to facilitate formal verification of code using such containers. The specification of this unit is compatible with SPARK 2014.

Note that although this container was designed with formal verification in mind, it may well be generally useful in that it is a simplified more efficient version than the one defined in the standard. In particular it does not have the complex overhead required to detect cursor tampering.