Choices for modelling binary packet protocol in SPARK

Choices for modelling binary packet protocol in SPARK

[xorque]

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

Re: Choices for modelling binary packet protocol in SPARK

[Phil Thornley]

On 18 July, 07:46, xorque <xorquew...@googlemail.com> wrote:
> Hello.
>
> I'm working on a protocol that uses many different binary packet
> types.
> They all inherit from one basic packet type.
>
[snip]

> 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?

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.

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

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

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. A tedious but
simple method is to use P1_Type and P2_Type as you have them for all
the internal processing, but with parallel record types that have
representation clauses suitable for UC to a byte array and operations
that convert between the two forms (these have to be explicit as
derived types aren't supported).

Phil Thornley

Re: Choices for modelling binary packet protocol in SPARK

[xorque]

On Jul 18, 12:23 pm, 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
>   Option    : P_Option_Type;
>   Timestamp : Integer;
>   P1        : P1_Type;
>   P2        : 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

Re: Choices for modelling binary packet protocol in SPARK

[Hibou57 (Yannick Duchêne)]

A link from my old book marks:
http://www.christ-usch-grein.homepage.t-online.de/Ada/Universe.html

Re: Choices for modelling binary packet protocol in SPARK

[Hibou57 (Yannick Duchêne)]

On 21 juil, 16:13, Hibou57 (Yannick Duchêne)
<yannick_duch...@yahoo.fr> wrote:
> A link from my old book marks:http://www.christ-usch-grein.homepage.t-online.de/Ada/Universe.html
Error in posting, sorry