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,b90aed4391a5846b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!a26g2000yqn.googlegroups.com!not-for-mail
From: xorque <xorquewasp@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Choices for modelling binary packet protocol in SPARK
Date: Sat, 18 Jul 2009 23:47:19 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <2c560673-0158-4968-b182-5aef9cfe8501@a26g2000yqn.googlegroups.com>
References: <f07b6888-eb5b-4953-a2c9-5acb5b682f4f@d4g2000yqa.googlegroups.com>
	<ea89c015-6d8d-4ef0-a0ed-f9960a980c99@d4g2000yqa.googlegroups.com>
NNTP-Posting-Host: 62.249.247.223
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1247986039 11991 127.0.0.1 (19 Jul 2009 06:47:19
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sun, 19 Jul 2009 06:47:19 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: a26g2000yqn.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:7146
Date: 2009-07-18T23:47:19-07:00
List-Id: <comp.lang.ada>

On Jul 18, 12:23=A0pm, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:
> As a rule, SPARK (and high-integrity code generally) avoids
> programming tricks - because the code becomes more error-prone for the
> author, reviewer and compiler.

Certainly.

> If the individual records are fairly small, is an ordinary record
> acceptable:
> type P_Type is record
> =A0 Option =A0 =A0: P_Option_Type;
> =A0 Timestamp : Integer;
> =A0 P1 =A0 =A0 =A0 =A0: P1_Type;
> =A0 P2 =A0 =A0 =A0 =A0: P2_Type;
> end record;

Unfortunately, some of the records may be up to 256kb in size (which
was the main motivation for a "union" type in the first place).

> Alternatively the language supports inheritance via tagged types, but
> with restrictions (no class-wide programming, only one derived type
> per package).

Right.

> A different approach would be to use Unchecked_Conversion for the
> individual record types, defining their layout with representation
> clauses to get the correct format of the byte array...

Yeah, I think this might be what I'll be doing.

xw