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
Well… I see that you got quite a bit done! 
Add formal bounded trees to SPARKlib · AdaCore/SPARKlib@76c0b01 · GitHub
Indeed The containers we just merged provide n-ary trees, so can be used to reason about trees with a fixed arity (number of branches from each node), such as binary search trees, ternary trees, quadtrees, etc.
We’re also evaluating multi-way trees (a.k.a. “rose trees”) where each node can have an arbitrary number of children.
That’s why Persistent Data Structures exist
The functional trees do something similar to this since they are immutable; they use reference counting internally so no copying is needed to insert a child into a tree.
It means they SHOULD be very efficient