Re: Choices for modelling binary packet protocol in SPARK

[xorque <xorquewasp@googlemail.com>]

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