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,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!d4g2000yqa.googlegroups.com!not-for-mail
From: xorque <xorquewasp@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Choices for modelling binary packet protocol in SPARK
Date: Fri, 17 Jul 2009 23:46:47 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <f07b6888-eb5b-4953-a2c9-5acb5b682f4f@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: 7bit
X-Trace: posting.google.com 1247899607 6078 127.0.0.1 (18 Jul 2009 06:46:47
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sat, 18 Jul 2009 06:46:47 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: d4g2000yqa.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:7126
Date: 2009-07-17T23:46:47-07:00
List-Id: <comp.lang.ada>

Hello.

I'm working on a protocol that uses many different binary packet
types.
They all inherit from one basic packet type.

Here's an example of a similar ASN.1 representation:

Base-Module
DEFINITIONS EXPLICIT TAGS ::=
BEGIN

P1-Type ::= SEQUENCE {
  value1 [0] INTEGER,
  value2 [1] INTEGER OPTIONAL
}

P2-Type ::= SEQUENCE {
  value1 [0] INTEGER,
  value2 [1] INTEGER,
  value3 [2] INTEGER
}

P-Data-Type ::= CHOICE {
  p1 [0] P1-Type,
  p2 [1] P2-Type
}

P-Type ::= SEQUENCE {
  timestamp [0] INTEGER,
  data      [1] P-Data-Type,
}

END

The equivalent in Ada might be:

type P1_Type is record
  Value1         : Integer;
  Value2_Present : Boolean;
  Value2         : Integer;
end record;

type P2_Type is record
  Value1 : Integer;
  Value2 : Integer;
  Value3 : Integer;
end record;

type P_Option_Type
  (P1_Selected,
   P2_Selected);

type P_Data_Type is (Option : P_Option_Type) is record
  case Option is
    when P1_Selected => P1 : P1_Type;
    when P2_Selected => P2 : P2_Type;
  end case;
end record;

type P_Type is (Option : P_Option_Type) record
  Timestamp : Integer;
  Data      : P_Data_Type (Option);
end record;

The program needs to be able to pack any and every type of packet
into a byte array to be written to a network socket. The part that
writes the data to the socket obviously doesn't care about the
contents of the packet and therefore only needs to see a byte
array or possibly a private Packet type that it can call a
general Pack procedure on in order to obtain a byte array for
writing. I would like to write the Pack procedure in SPARK as
it seems like it would be the exact type of 'pure' code that
SPARK is suited to.

I'm not sure, exactly, with a lack of variant records, how I'm
meant to model this in SPARK.

Am I going to be writing enormous case statements or is there
some clever way to handle this kind of thing?

xw