SPARK and unbounded tree structures

SPARK and unbounded tree structures

[xorquewasp]

I'm going to be working on a compiler for a domain-specific functional
language soon. For obvious reasons, I'd like to use SPARK, if
possible.

The problem: The compiler is inevitably going to involve tree
structures
of a completely unbounded size. It's also inevitably going to involve
variant records.

Are there any real world examples of using SPARK in situations that
involve large dynamic data structures? As far as I can tell given my
week
or so of experience with SPARK, this would basically involve --# hide -
ing
most of the program and would essentially make the whole exercise
pointless.

Re: SPARK and unbounded tree structures

[Rod Chapman]

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

Re: SPARK and unbounded tree structures

[Phil Thornley]

On 11 June, 08:35, Rod Chapman <roderick.chap...@googlemail.com>
wrote:
...

> 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.

There are some iterative tree algorithms by Julienne Walker at
eternallyconfuzzled.com.

(A variant of the Red-Black tree algorithm there has been used on a
SPARK project.)

Phil Thornley

Re: SPARK and unbounded tree structures

[xorque]

Thanks again, both of you.

Re: SPARK and unbounded tree structures

[Stephen Leake]

xorquewasp@googlemail.com writes:

> I'm going to be working on a compiler for a domain-specific functional
> language soon. For obvious reasons, I'd like to use SPARK, if
> possible.

Ada is an obvious choice for this project, but SPARK is not.

SPARK is a good fit for _high integrity_ software, where you _must_ be
able to prove precise statements about the program's behavior.

Compilers are not that. They are far too complex for tools like SPARK
to handle (given the current state of the art), only in part because
of the problem you cite here.

All compilers have bugs. That's the state of the art. That's why users
must test their code, and assume the compiler has bugs.

-- 
-- Stephe