Re: Choices for modelling binary packet protocol in SPARK

[Phil Thornley <phil.jpthornley@googlemail.com>]

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