Formal Containers

We have added a new page describing Formal Containers to the Hi-Lite project. It describes a new version of the API for Ada definite containers, designed to simplify the annotation process. An implementation of these containers will be usable in critical programs. It is really interesting to have containers for critical systems, since they are often a good trade-off for ad-hoc, pointer-based structures which make users’ code hard to certify. Since they have been formally axiomatized, these containers will be part of the Ada subset that can be formally proved correct in the context of Hi-Lite.
This entry was posted in Open-DO News. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

Post a Comment

Your email is never published nor shared. Required fields are marked *

  • Categories

  • Open-DO Projects

  • Contact

    info @