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