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 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,7dea5b3f9fad4e83
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!newsfeed01.sul.t-online.de!t-online.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 21 Jul 2009 12:40:29 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Thunderbird 2.0.0.22 (Macintosh/20090605)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: SPARK left/right shift.
References: 
 <9d0eb92b-bb21-40eb-ac6d-2e1e829b95cc@s15g2000yqs.googlegroups.com>
 	<3642aa53-ed44-4562-9be5-ebc2cfc1c92b@a26g2000yqn.googlegroups.com>
 <6a8fc5de-7a2d-429c-81af-e1ac68e85b1f@t13g2000yqt.googlegroups.com>
In-Reply-To: 
 <6a8fc5de-7a2d-429c-81af-e1ac68e85b1f@t13g2000yqt.googlegroups.com>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Message-ID: <4a659b1d$0$30227$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 21 Jul 2009 12:40:29 CEST
NNTP-Posting-Host: 16aae0ae.newsspool1.arcor-online.net
X-Trace: 
 DXC=KNZ3_gFIe=O[6=1B@oB@@@ic==]BZ:afN4Fo<]lROoRA^YC2XCjHcbIQMh\\V]IH0B;9OJDO8_SKFNSZ1n^B98iJFkhICCbLWoI
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news2.google.com comp.lang.ada:7211
Date: 2009-07-21T12:40:29+02:00
List-Id: <comp.lang.ada>

xorque schrieb:

> I'm not currently writing anything that could be described
> as "high-integrity" but I try to use SPARK wherever possible
> as I do care deeply about software quality.

Can I second this?  In writing a double buffer properly,
in particular when varying length characters need to be
handled, SPARK is really helpful, if only to sort out
and document the author's assumptions, omissions, and errors.

Same for a live topsorted structure that is waiting on
my shelf to be finished.