12.13 Ada.Containers.Functional_Vectors (a-cofuve.ads)

This child of Ada.Containers defines immutable vectors. These containers are unbounded and may contain indefinite elements. Furthermore, to be usable in every context, they are neither controlled nor limited. As they are functional, that is, no primitives are provided which would allow modifying an existing container, these containers can still be used safely.

Their API features functions creating new containers from existing ones. As a consequence, these containers are highly inefficient. They are also memory consuming, as the allocated memory is not reclaimed when the container is no longer referenced. Thus, they should in general be used in ghost code and annotations, so that they can be removed from the final executable. The specification of this unit is compatible with SPARK 2014.