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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,6941f5cd4f1d4739,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!c10g2000yqi.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: SPARK - an idea for high integrity data structures
Date: Tue, 20 Jul 2010 05:40:42 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <9ac8feb3-5b79-41b1-a124-df211039c1bc@c10g2000yqi.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1279629642 3081 127.0.0.1 (20 Jul 2010 12:40:42
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 20 Jul 2010 12:40:42 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: c10g2000yqi.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:12479
Date: 2010-07-20T05:40:42-07:00
List-Id: <comp.lang.ada>

I have had a hobby project for a while to create SPARK versions of
data structures, supported by partial proofs of correctness.

However, if the proofs are tackled in the most obvious way then the
effort required to show that the relevant data structure invariant is
maintained by each operation grows out of all proportion to the size
of the code being proved, and it would be easier to validate the code
directly than to validate all the proof artefacts (annotations and
rules) that are generated for the proof.

So I have recently tried an alternative approach that shows some
potential for completing the proofs without requiring disproportionate
effort.

The idea is to determine, for each path through an operation that
exports a value of the data structure, the relationship between the
imported value and exported value and to create a single proof rule
that encapsulates that transformation.  If the rule proves the
postcondition VC generated for the path then the code implements the
transformation.

This is clearly a less rigorous approach than proving that the code
maintains all the individual conditions within the invariant, but it
is much more practicable.

As an example of this approach I have completed the proofs for an
ordered list of integers and put this up on http://www.sparksure.com
(I have included a stack and a queue as well, but neither of these
require data structure invariants).

I am very interested in all comments that anybody might have about
this idea - either here on cla or via the email address on the
website.

Phil Thornley