Next: Ada Containers Formal_Hashed_Maps a-cfhama ads, Previous: Ada Characters Wide_Wide_Latin_9 a-chzla9 ads, Up: The GNAT Library
a-cfdlli.ads)This child of Ada.Containers defines a modified version of the Ada 2005 container for doubly linked lists, 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.