AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
107 stars 7 forks source link

Shorter syntax for integer types covering entire value range #1250

Open treiher opened 2 years ago

treiher commented 2 years ago

Context and Problem Statement

Declaring an integer type which covers the entire value range can be quite cumbersome:

type T is range 0 .. 2 ** 16 - 1 with Size => 16;

Use Cases

There are many cases in message formats of real world protocols where such integers are required.

Considered Options

O1 Optional Size aspect

type T is range 0 .. 2 ** 16 - 1;

+ No new keyword Implicit determination of type size could be confusing for user

O2 Box instead value range

type T is range <> with Size => 16;

+ No new keyword range <> does also occur in Ada, but in different context, so could be confusing for Ada programmers

O3 New keyword

O3.1

type T is size 16;

+ Concise New keyword (with the same name as an existing aspect)

O3.2

type T is unsigned 16;

+ Concise + Can be extended by signed keyword for signed integer types New keyword

O4 Reuse syntax of modular types

type T is mod 2**16;

Well-known syntax for Ada programmers, but different semantics as in Ada (cf. #727)

Decision Outcome

O3.2