From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!21g2000vbk.googlegroups.com!not-for-mail
From: xorquewasp@googlemail.com
Newsgroups: comp.lang.ada
Subject: SPARK and unbounded tree structures
Date: Wed, 10 Jun 2009 09:52:28 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <06f0b9ca-3c00-44e8-9a52-63c840ed0abe@21g2000vbk.googlegroups.com>
NNTP-Posting-Host: 81.86.41.187
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1244652749 19894 127.0.0.1 (10 Jun 2009 16:52:29
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 10 Jun 2009 16:52:29 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: 21g2000vbk.googlegroups.com; posting-host=81.86.41.187;
	posting-account=D9GNUgoAAAAmg7CCIh9FhKHNAJmHypsp
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.7)
	Gecko/2009030814 Iceweasel/3.0.9 (Debian-3.0.9-1),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6417
Date: 2009-06-10T09:52:28-07:00
List-Id: <comp.lang.ada>

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.