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-Thread: a07f3367d7,7dea5b3f9fad4e83
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!t13g2000yqt.googlegroups.com!not-for-mail
From: xorque <xorquewasp@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK left/right shift.
Date: Tue, 21 Jul 2009 03:00:18 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <6a8fc5de-7a2d-429c-81af-e1ac68e85b1f@t13g2000yqt.googlegroups.com>
References: 
 <9d0eb92b-bb21-40eb-ac6d-2e1e829b95cc@s15g2000yqs.googlegroups.com>
	<3642aa53-ed44-4562-9be5-ebc2cfc1c92b@a26g2000yqn.googlegroups.com>
NNTP-Posting-Host: 62.249.247.223
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1248170419 31357 127.0.0.1 (21 Jul 2009 10:00:19
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 21 Jul 2009 10:00:19 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: t13g2000yqt.googlegroups.com; posting-host=62.249.247.223;
	posting-account=D9GNUgoAAAAmg7CCIh9FhKHNAJmHypsp
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.11)
	Gecko/2009061212 Iceweasel/3.0.9 (Debian-3.0.9-1),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:7209
Date: 2009-07-21T03:00:18-07:00
List-Id: <comp.lang.ada>

Rod Chapman wrote:
> xorque,
>  If it's not a dumb question: what exactly are you trying to
> implement with SPARK?  It seems rather ambitious - you've
> been pushing the boundaries a fair bit....

Currently, a UTF-8 encoder/decoder.

Quite a few questions I've posted on here have been related
to "toy" projects testing what can be done sanely with this
degree of verification in Ada. I've rarely been disappointed.

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.