Next: Ada.Containers.Formal_Ordered_Maps (a-cforma.ads), Previous: Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads), Up: The GNAT Library
Ada.Containers.Formal_Hashed_Sets (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.