AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

Apache License 2.0

104 stars 6 forks source link

Document specification features #342

Open treiher opened 4 years ago

treiher commented 4 years ago

Specification Features

Main elements

Type: Modular Integer
Type: Range Integer
Type: Enumeration
Type: Enumeration (always valid)
Type: Boolean
Type: Message
Type: Derived message
Type: Sequence of scalar (modular, range enumerations)
Type: Sequence of message
Type refinement (specify type of opaque field)

Message type

Field type: Scalar (modular, range, enumeration)
Field type: Sequence of message
Field type: Sequence of scalar
Field type: Message
Field type: Opaque
Field length statically defined by type size
Field length statically defined by value
Field length dynamically defined by value of other fields
Field length dynamically defined by available space
Field condition: Logical expression referring to field value/length/first/last
Field condition: Logical expression referring to message length/last
Optional field (occurrence determined by condition)
Overlayed field (first bit on some position, same length)
Checksum aspect
Parameters

Session

Declarations
- Renaming declaration
- Variable declaration
Expressions
- Aggregates
- Attribute expressions
  - Head attribute
  - Has_Data attribute
  - Opaque attribute
  - Valid attribute
- Bindings
- Calls
- Conversions
- List comprehensions
- Quantified expressions
- Selected expressions
Session parameters
- Channels
- Functions
  - Allowed parameter types
    - Definite messages
    - Opaque fields of messages
    - Scalars
  - Allowed return types
    - Definite messages
    - Scalars
- Private types
States
- State actions
  - Assignment statements
  - Append attribute statements
  - Extend attribute statements
  - Read attribute statements
  - Reset attribute statements
  - Write attribute statements
- State declarations
  - Renaming declarations
  - Variable declarations
- Exception transition
- Null state
- State transitions

Structure

Use types of other specification file

Constraints

Names are case insensitive

senier commented 4 years ago

This also is related to #223.