Re: SPARK and unbounded tree structures

[Rod Chapman <roderick.chapman@googlemail.com>]

On Jun 10, 5:52 pm, xorquew...@googlemail.com wrote:
> Are there any real world examples of using SPARK in situations that
> involve large dynamic data structures?

Only the SPARK Examiner itself, and in that even the data
structures are ultimately bounded.

Remember - SPARK is principally designed for the construction
of hard real-time and embedded systems, where the "size"
of the problem domain is known well in advance - hence
most SPARK system use data-structures with a fixed upper
limit.

You also need to consider that SPARK is non-recurive, so
walking and building such data structures nees to be
done with wholly iterative algorithms, which is an unusual
programming style to say the least.

In short: it sounds like SPARK is unlikely to be a good
choice for this style of application. If you _really_ want
to see how it's done, then see the Examiner sources - data structures
like stree.ads and heap.ads, and the tree-walking algorithms in
sem-compunit.adb for example.

Yours,
 Rod Chapman, SPARK Team