Another news that may have flown under the radar for some… SPARKlib added support for trees back in late November. You can see the commit and code here: Add functional trees to SPARKlib · AdaCore/SPARKlib@a7d8ec3 · GitHub
Best regards,
Fer
Are there plans to make it available with alire?
We’re also working on the formal tree containers too!
SPARKlib is already bundled with GNATprove, which is available in Alire. Though I would like to eventually get it into its own create which will improve usability.
1 Like
Yes, gnatprove is a heavy dependency (around 1Gb as I remember). And some may want to use spark libs without writing themself spark code. A separate crate would be nice.
Though I would like to eventually get it into its own create which will improve usability.
I have plans for that 
1 Like
“functional” as in functional programming?
Is this something else?
SPARKlib has two kinds of containers: functional containers and formal containers.
The formal containers are the ones you’d typically use in your program. They are similar to the Ada containers, but with contracts to allow proving correct usage in client code with the SPARK tools.
The functional containers are simpler, mathematical-like containers which are often needed to model complex data structures. So that they can be used safely, these containers are functional, that is, no primitives are provided which would allow modifying an existing container. Instead, their API features functions creating new containers from existing ones. As a consequence, the functional containers are highly inefficient, but is generally used in ghost code/contracts and annotations so that they can be removed from the final executable while still being available for proof.
You can read more about SPARKlib and its containers here: 5.11. SPARK Libraries — SPARK User's Guide 27.0w
As Fer mentioned, we recently added a functional (mathematical-like) version of the tree container, and we are now working on the formal version of n-ary and multi-way tree containers.
5 Likes