Next: Ada Containers Formal_Hashed_Sets a-cfhase ads, Previous: Ada Containers Formal_Doubly_Linked_Lists a-cfdlli ads, Up: The GNAT Library
a-cfhama.ads)This child of Ada.Containers defines a modified version of the Ada 2005 container for hashed maps, 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.