From 568806971946b4f6b26378e0e78516f06e147a29 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Fri, 23 Jul 2021 13:24:41 +0200 Subject: [PATCH] Improve documentation - Use AsciiDoc instead of Markdown - Adapt documentation check to AsciiDoc format - Improve layout of syntax rules - Add cross references between syntax rules Ref. #703 --- README.md => README.adoc | 215 ++--- doc/Development.md | 4 +- doc/Language-Reference.adoc | 1625 +++++++++++++++++++++++++++++++++++ doc/Language-Reference.md | 1410 ------------------------------ setup.py | 2 +- tests/unit/cli_test.py | 6 +- tools/check_doc.py | 32 +- 7 files changed, 1761 insertions(+), 1533 deletions(-) rename README.md => README.adoc (58%) create mode 100644 doc/Language-Reference.adoc delete mode 100644 doc/Language-Reference.md diff --git a/README.md b/README.adoc similarity index 58% rename from README.md rename to README.adoc index 44f94358d4..0b34f65aa2 100644 --- a/README.md +++ b/README.adoc @@ -1,18 +1,14 @@ -# [![RecordFlux](doc/img/logo.svg)](https://github.com/Componolit/RecordFlux/) +== https://github.com/Componolit/RecordFlux/[image:doc/img/logo.svg[RecordFlux]] -[![PyPI](https://img.shields.io/pypi/v/RecordFlux?color=blue)](https://pypi.org/project/RecordFlux/) -[![Python Versions](https://img.shields.io/badge/python-3.7%20%7C%203.8%20%7C%203.9-blue.svg)](https://python.org/) -[![Checked with mypy](http://www.mypy-lang.org/static/mypy_badge.svg)](http://mypy-lang.org/) -[![Tests](https://github.com/Componolit/RecordFlux/workflows/tests/badge.svg)](https://github.com/Componolit/RecordFlux/actions) -[![CII Best Practices](https://bestpractices.coreinfrastructure.org/projects/5052/badge)](https://bestpractices.coreinfrastructure.org/projects/5052) +https://pypi.org/project/RecordFlux/[image:https://img.shields.io/pypi/v/RecordFlux?color=blue[PyPI]] https://python.org/[image:https://img.shields.io/badge/python-3.7%20%7C%203.8%20%7C%203.9-blue.svg[Python Versions]] http://mypy-lang.org/[image:http://www.mypy-lang.org/static/mypy_badge.svg[Checked with mypy]] https://github.com/Componolit/RecordFlux/actions[image:https://github.com/Componolit/RecordFlux/workflows/tests/badge.svg[Tests]] https://bestpractices.coreinfrastructure.org/projects/5052[image:https://bestpractices.coreinfrastructure.org/projects/5052/badge[CII Best Practices]] RecordFlux is a toolset for the formal specification of messages and the generation of verifiable binary parsers and message generators. -## Message Specification +=== Message Specification -The RecordFlux specification language is a domain-specific language to formally specify message formats of existing real-world binary protocols. Its syntax is inspired by [Ada](https://www.adacore.com/about-ada). A detailed description of the language elements can be found in the [Language Reference](/doc/Language-Reference.md). +The RecordFlux specification language is a domain-specific language to formally specify message formats of existing real-world binary protocols. Its syntax is inspired by https://www.adacore.com/about-ada[Ada]. A detailed description of the language elements can be found in the link:/doc/Language-Reference.adoc[Language Reference]. -Message specifications are automatically verified using the [Z3 theorem prover](https://github.com/Z3Prover/z3). The following invariants are proven at the specification level: +Message specifications are automatically verified using the https://github.com/Z3Prover/z3[Z3 theorem prover]. The following invariants are proven at the specification level: * Field conditions are mutually exclusive * Field conditions do not contradict each other @@ -24,9 +20,9 @@ Message specifications are automatically verified using the [Z3 theorem prover]( * Message fields cover all bits of a message on all paths * Overlaid fields are congruent with exactly one other field -## SPARK Code Generation +=== SPARK Code Generation -Message parsers and generators are generated based on message specifications. The generated parser allows to validate and dissect messages and thereby respects all specified restrictions between message fields and related messages. The generated message generator enables the creation of messages according to the message specification. By using [SPARK](https://www.adacore.com/about-spark) we are able to prove the absence of runtime errors and prevent the incorrect usage of the generated code (e.g., enforce that a field of a message is validated before accessed). +Message parsers and generators are generated based on message specifications. The generated parser allows to validate and dissect messages and thereby respects all specified restrictions between message fields and related messages. The generated message generator enables the creation of messages according to the message specification. By using https://www.adacore.com/about-spark[SPARK] we are able to prove the absence of runtime errors and prevent the incorrect usage of the generated code (e.g., enforce that a field of a message is validated before accessed). Multiple packages are generated for a specification. All basic types like integers, enumerations and sequences are collectively declared in one package. For each message a child package is generated which contains validation, accessor and setter functions for every field of the message. @@ -34,29 +30,30 @@ A user of the generated code has to validate a message field or the whole messag The `rflx` tool is used to verify a specification and generate SPARK code based on it. It offers the sub-commands `check` and `generate` for this purpose. The sub-command `graph` allows to generate images of the graph representations of messages in a specification. -## Python Library +=== Python Library PyRFLX is a Python library for rapid-prototyping and validation. It uses RecordFlux specifications for parsing and generation of messages and validates the formal specification at runtime. It can be used by importing `rflx.pyrflx`. -By default assertions and contracts are executed to ensure correct functionality. For improved performance these additional checks can be disabled by running Python with the [`-O`](https://docs.python.org/3/using/cmdline.html#cmdoption-o) switch. +By default assertions and contracts are executed to ensure correct functionality. For improved performance these additional checks can be disabled by running Python with the https://docs.python.org/3/using/cmdline.html#cmdoption-o[`-O`] switch. -## Example +=== Example In the following, the complete process of specifying a message, generating code, and using the generated code is demonstrated using a small example. -### Specification +==== Specification The following sample specification describes a protocol `TLV` with one message type `Message` consisting of three fields: -- A field `Tag` of 2 bit length, -- a field `Value_Length` of 14 bit length, and -- a field `Value`, whose length is specified by the value in `Value_Length`. +* A field `Tag` of 2 bit length, +* a field `Value_Length` of 14 bit length, and +* a field `Value`, whose length is specified by the value in `Value_Length`. The `Tag` can have two valid values: `1` (`Msg_Data`) and `3` (`Msg_Error`). In case `Tag` has a value of `1` the fields `Value_Length` and `Value` follow. `Message` contains only the `Tag` field, if the value of `Tag` is `3`. All other values of `Tag` lead to an invalid message. -The structure of messages is often non-linear because of optional fields. For this reason the specification uses a graph-based representation. The order of fields is defined by then clauses. Then clauses are also used to state conditions and aspects of the following field. A more detailed description can be found in the [Language Reference](doc/Language-Reference.md#message-type). +The structure of messages is often non-linear because of optional fields. For this reason the specification uses a graph-based representation. The order of fields is defined by then clauses. Then clauses are also used to state conditions and aspects of the following field. A more detailed description can be found in the link:doc/Language-Reference.adoc#message-type[Language Reference]. -```Ada RFLX +[source,ada,rflx] +---- package TLV is type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 8; @@ -76,21 +73,23 @@ package TLV is end message; end TLV; -``` +---- -### Generating Code +==== Generating Code With the sub-command `check` the correctness of the given specification file can be checked. -```Console +[source,console] +---- $ rflx check tests/data/specs/tlv.rflx Parsing tests/data/specs/tlv.rflx Processing TLV -``` +---- The sub-command `generate` is used to generate the code based on the specification. The target directory and the specification files have to be given. -```Console +[source,console] +---- $ mkdir /tmp/generated $ rflx generate -d /tmp/generated tests/data/specs/tlv.rflx Parsing tests/data/specs/tlv.rflx @@ -111,70 +110,71 @@ Creating /tmp/generated/rflx-rflx_generic_types.adb Creating /tmp/generated/rflx-rflx_message_sequence.adb Creating /tmp/generated/rflx-rflx_scalar_sequence.adb Creating /tmp/generated/rflx.ads -``` +---- -### Using the Generated Code +==== Using the Generated Code All scalar types defined in the specification are represented by a similar Ada type in the generated code. For `TLV` the following types are defined in the package `RFLX.TLV`: -- `type Tag is (Msg_Data, Msg_Error) with Size => 2` -- `for Tag use (Msg_Data => 1, Msg_Error => 3);` -- `type Length is mod 2**14` +* `type Tag is (Msg_Data, Msg_Error) with Size => 2` +* `for Tag use (Msg_Data => 1, Msg_Error => 3);` +* `type Length is mod 2**14` All types and subprograms related to `Message` can be found in the package `RFLX.TLV.Message`: -- `type Context` - - Stores buffer and internal state -- `procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr)` - - Initialize context with buffer -- `procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr; First, Last : Types.Bit_Index)` - - Initialize context with buffer and explicit bounds -- `procedure Take_Buffer (Ctx : in out Context; Buffer : out Types.Bytes_Ptr)` - - Get buffer and remove it from context (note: buffer cannot put back into context, thus further verification of message is not possible after this action) -- `function Has_Buffer (Ctx : Context) return Boolean` - - Check if context contains buffer (i.e. non-null pointer) -- `procedure Verify (Ctx : in out Context; Fld : Field)` - - Verify validity of field -- `procedure Verify_Message (Ctx : in out Context)` - - Verify all fields of message -- `function Structural_Valid (Ctx : Context; Fld : Field) return Boolean` - - Check if composite field is structural valid (i.e. location and size of field is correct, but content is not necessarily valid) -- `function Present (Ctx : Context; Fld : Field) return Boolean` - - Check if composite field is structural valid and has non-zero size -- `function Valid (Ctx : Context; Fld : Field) return Boolean` - - Check if field is valid (i.e. it has valid structure and valid content) -- `function Incomplete (Ctx : Context; Fld : Field) return Boolean` - - Check if buffer was too short to verify field -- `function Structural_Valid_Message (Ctx : Context) return Boolean` - - Check if all fields of message are at least structural valid -- `function Valid_Message (Ctx : Context) return Boolean` - - Check if all fields of message are valid -- `function Incomplete_Message (Ctx : Context) return Boolean` - - Check if buffer was too short to verify message -- `function Get_Tag (Ctx : Context) return Tag_Type` - - Get value of `Tag` field -- `function Get_Length (Ctx : Context) return Length_Type` - - Get value of `Length` field -- `generic with procedure Process_Value (Value : Types.Bytes); procedure Get_Value (Ctx : Context)` - - Access content of `Value` field -- `function Valid_Next (Ctx : Context; Fld : Field) return Boolean` - - Check if field is potential next field -- `procedure Set_Tag (Ctx : in out Context; Value : Tag)` - - Set value of `Tag` field -- `procedure Set_Length (Ctx : in out Context; Value : Length)` - - Set value of `Length` field -- `procedure Set_Value_Empty (Ctx : in out Context; Value : Types.Bytes)` - - Set empty `Value` field -- `procedure Set_Value (Ctx : in out Context; Value : Types.Bytes)` - - Set content of `Value` field -- `generic with procedure Process_Value (Value : out Types.Bytes); procedure Generic_Set_Value (Ctx : in out Context)` - - Set content of `Value` field -- `procedure Initialize_Value (Ctx : in out Context)` - - Initialize `Value` field (precondition to switch context for generating contained message) +* `type Context` +** Stores buffer and internal state +* `procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr)` +** Initialize context with buffer +* `procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr; First, Last : Types.Bit_Index)` +** Initialize context with buffer and explicit bounds +* `procedure Take_Buffer (Ctx : in out Context; Buffer : out Types.Bytes_Ptr)` +** Get buffer and remove it from context (note: buffer cannot put back into context, thus further verification of message is not possible after this action) +* `function Has_Buffer (Ctx : Context) return Boolean` +** Check if context contains buffer (i.e. non-null pointer) +* `procedure Verify (Ctx : in out Context; Fld : Field)` +** Verify validity of field +* `procedure Verify_Message (Ctx : in out Context)` +** Verify all fields of message +* `function Structural_Valid (Ctx : Context; Fld : Field) return Boolean` +** Check if composite field is structural valid (i.e. location and size of field is correct, but content is not necessarily valid) +* `function Present (Ctx : Context; Fld : Field) return Boolean` +** Check if composite field is structural valid and has non-zero size +* `function Valid (Ctx : Context; Fld : Field) return Boolean` +** Check if field is valid (i.e. it has valid structure and valid content) +* `function Incomplete (Ctx : Context; Fld : Field) return Boolean` +** Check if buffer was too short to verify field +* `function Structural_Valid_Message (Ctx : Context) return Boolean` +** Check if all fields of message are at least structural valid +* `function Valid_Message (Ctx : Context) return Boolean` +** Check if all fields of message are valid +* `function Incomplete_Message (Ctx : Context) return Boolean` +** Check if buffer was too short to verify message +* `function Get_Tag (Ctx : Context) return Tag_Type` +** Get value of `Tag` field +* `function Get_Length (Ctx : Context) return Length_Type` +** Get value of `Length` field +* `generic with procedure Process_Value (Value : Types.Bytes); procedure Get_Value (Ctx : Context)` +** Access content of `Value` field +* `function Valid_Next (Ctx : Context; Fld : Field) return Boolean` +** Check if field is potential next field +* `procedure Set_Tag (Ctx : in out Context; Value : Tag)` +** Set value of `Tag` field +* `procedure Set_Length (Ctx : in out Context; Value : Length)` +** Set value of `Length` field +* `procedure Set_Value_Empty (Ctx : in out Context; Value : Types.Bytes)` +** Set empty `Value` field +* `procedure Set_Value (Ctx : in out Context; Value : Types.Bytes)` +** Set content of `Value` field +* `generic with procedure Process_Value (Value : out Types.Bytes); procedure Generic_Set_Value (Ctx : in out Context)` +** Set content of `Value` field +* `procedure Initialize_Value (Ctx : in out Context)` +** Initialize `Value` field (precondition to switch context for generating contained message) A simple program to parse a `TLV.Message` could be as follows: -```Ada +[source,ada] +---- with Ada.Text_IO; with RFLX.RFLX_Builtin_Types; with RFLX.TLV.Message; @@ -202,13 +202,14 @@ begin Ada.Text_IO.Put_Line ("Invalid message"); end if; end Main; -``` +---- In case that a valid message is contained in `Buffer` the value of `Tag` is read. If the value of `Tag` is `Msg_Data` and the `Value` field is present, the content of `Value` can be accessed. A `TLV.Message` can be generated as follows: -```Ada +[source,ada] +---- with Ada.Text_IO; with RFLX.RFLX_Builtin_Types; use type RFLX.RFLX_Builtin_Types.Length, RFLX.RFLX_Builtin_Types.Bytes; with RFLX.TLV.Message; @@ -231,14 +232,14 @@ begin Ada.Text_IO.Put_Line ("Unexpected"); end if; end Main; -``` +---- -### Using the Python Library +==== Using the Python Library The following code shows how PyRFLX can be used to parse and generate messages in Python: - -```Python +[source,python] +---- import sys from rflx.pyrflx import MessageValue, PyRFLX @@ -263,51 +264,53 @@ def create_message() -> MessageValue: if parse_message(b"\x01\x00\x04\x01\x02\x03\x04") != create_message(): sys.exit("Error") -``` +---- -## Installation +=== Installation As a prerequisite, the following dependencies need to be installed: -- [GNAT Community](https://www.adacore.com/download) >= 2021 -- [GMP](https://gmplib.org/) is provided as a package for various distributions, e.g., `libgmp-dev` (Debian/Ubuntu), `gmp-devel` (Fedora) or `gmp` (Arch Linux). -- Optional: [Graphviz](https://graphviz.org/) is required for plotting graphs. It is provided as package `graphviz` for various distributions. +* https://www.adacore.com/download[GNAT Community] >= 2021 +* https://gmplib.org/[GMP] is provided as a package for various distributions, e.g., `libgmp-dev` (Debian/Ubuntu), `gmp-devel` (Fedora) or `gmp` (Arch Linux). +* Optional: https://graphviz.org/[Graphviz] is required for plotting graphs. It is provided as package `graphviz` for various distributions. RecordFlux can be installed from PyPI: -```Console +[source,console] +---- $ pip3 install RecordFlux -``` +---- By default the following dependencies are installed: -- [icontract](https://github.com/Parquery/icontract) -- [PyDotPlus](https://github.com/carlos-jenkins/pydotplus) -- [Z3](https://github.com/Z3Prover/z3) -- [RecordFlux parser](https://github.com/Componolit/RecordFlux-language) +* https://github.com/Parquery/icontract[icontract] +* https://github.com/carlos-jenkins/pydotplus[PyDotPlus] +* https://github.com/Z3Prover/z3[Z3] +* https://github.com/Componolit/RecordFlux-language[RecordFlux parser] Optionally, the GNAT Studio IDE integration for RecordFlux can be installed. It enables syntax highlighting for RecordFlux specifications and allows for running RecordFlux from within GNAT Studio. In the RecordFlux source directory do: -```Console +[source,console] +---- $ make install_gnatstudio -``` +---- -## Contribution and Feedback +=== Contribution and Feedback -Contributions and feedback to RecordFlux are very welcome. To discuss a bug or an enhancement, [open a ticket on GitHub](https://github.com/Componolit/RecordFlux/issues/new/choose) and select the appropriate issue template. Please give sufficient information about your issue, the software version you are using and your environment such that the developers can understand and (if necessary) reproduce the problem. If none of the provided issue templates fit your needs, feel free to open [a blank issue](https://github.com/Componolit/RecordFlux/issues/new). +Contributions and feedback to RecordFlux are very welcome. To discuss a bug or an enhancement, https://github.com/Componolit/RecordFlux/issues/new/choose[open a ticket on GitHub] and select the appropriate issue template. Please give sufficient information about your issue, the software version you are using and your environment such that the developers can understand and (if necessary) reproduce the problem. If none of the provided issue templates fit your needs, feel free to open https://github.com/Componolit/RecordFlux/issues/new[a blank issue]. -See [the development documentation](/doc/Development.md) on how to contribute to RecordFlux. +See link:/doc/Development.md[the development documentation] on how to contribute to RecordFlux. -## Limitations +=== Limitations -A list of known limitations for version 0.4.1 can be found [here](https://github.com/Componolit/RecordFlux/issues?q=is%3Aissue+label%3Alimitation+label%3Av0.4.1). +A list of known limitations for version 0.4.1 can be found https://github.com/Componolit/RecordFlux/issues?q=is%3Aissue+label%3Alimitation+label%3Av0.4.1[here]. -## Background +=== Background More information about the theoretical background can be found in our paper: -Reiher T., Senier A., Castrillon J., Strufe T. (2020) RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers. In: Arbab F., Jongmans SS. (eds) Formal Aspects of Component Software. FACS 2019. Lecture Notes in Computer Science, vol 12018. Springer, Cham ([paper](https://doi.org/10.1007/978-3-030-40914-2_9), [preprint](https://arxiv.org/abs/1910.02146)) +Reiher T., Senier A., Castrillon J., Strufe T. (2020) RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers. In: Arbab F., Jongmans SS. (eds) Formal Aspects of Component Software. FACS 2019. Lecture Notes in Computer Science, vol 12018. Springer, Cham (https://doi.org/10.1007/978-3-030-40914-2_9[paper], https://arxiv.org/abs/1910.02146[preprint]) -## Licence +=== Licence This software is licensed under the `AGPL-3.0`. See the `LICENSE` file for the full license text. diff --git a/doc/Development.md b/doc/Development.md index 441db5d71f..cbf5547206 100644 --- a/doc/Development.md +++ b/doc/Development.md @@ -2,7 +2,7 @@ ## Installation -The required dependencies are listed in the [README](../README.md#installation). After cloning the repository, `pip` can be used to install the project in editable mode. The use of a [virtual environment](https://docs.python.org/3/tutorial/venv.html) is recommended. +The required dependencies are listed in the [README](../README.adoc#installation). After cloning the repository, `pip` can be used to install the project in editable mode. The use of a [virtual environment](https://docs.python.org/3/tutorial/venv.html) is recommended. ```Console $ virtualenv -p python3 venv @@ -28,6 +28,6 @@ We accept pull requests [via GitHub](https://github.com/Componolit/RecordFlux/co When submitting a pull request, your topic branch should be rebased to the current upstream `main` branch. Verify that all automatic checks performed by `make check`, `make test` and `make prove` succeed before submitting the PR. For Python code we follow and automatically enforce the coding style of [Black](https://pypi.org/project/black/). You can format your code automatically using the `make format` target on the command line. For Ada code (examples as well as generated code) please follow [our Ada style guide](https://github.com/Componolit/ada-style). -We enforce 100% branch coverage for Python code using [pytest](https://pytest.org). Make sure to add relevant test cases to achieve that for your code. See [the test documentation](/tests/README.md) and have a look at the existing test cases in the `tests` directory to get an idea of the structure of our test suite. Our Python code is also statically type-checked using [mypy](http://mypy-lang.org/). Make sure to include the required type annotations with your code. +We enforce 100% branch coverage for Python code using [pytest](https://pytest.org). Make sure to add relevant test cases to achieve that for your code. See [the test documentation](/tests/README.adoc) and have a look at the existing test cases in the `tests` directory to get an idea of the structure of our test suite. Our Python code is also statically type-checked using [mypy](http://mypy-lang.org/). Make sure to include the required type annotations with your code. Your code will be reviewed by at least one core developer before inclusion into the project. Don't be discouraged should we have many comments and ask you for a lot of changes to your pull request. This even happens to the most experienced developers in our project and we consider these discussions an essential part of the development process and a necessity to maintain high quality. Don't hesitate to open an issue if you have any question or submit the pull request in draft mode first. diff --git a/doc/Language-Reference.adoc b/doc/Language-Reference.adoc new file mode 100644 index 0000000000..a3f9dce3d6 --- /dev/null +++ b/doc/Language-Reference.adoc @@ -0,0 +1,1625 @@ +== Language Reference + +The specification language describes protocol message formats based on types. For each type of the specification language a description of its syntax and semantics and an example is given. A simple variant of Backus-Naur Form is used to describe the syntax. Reserved keywords and literals are marked in *bold*. References to syntactic categories are xref:none[highlighted]. To convey some semantic information the name of some syntactic categories are prefixed by a non-highlighted part. Syntactic categories with prefixes are equivalent to the category without the prefix. The following basic elements are used to describe the syntax of the language: + +[[syntax-name]] +name: A name consists of alphanumeric characters and underscores. By convention a name starts with a capital and after each underscore follows a capital as well (e.g., Mixed_Case_With_Underscores). + +[[syntax-number]] +number: A number consists of numerical digits. An underscore can be added between two digits to improve readability. + +[[syntax-mathematical_expression]] +mathematical_expression: A mathematical expression consists of numbers and names combined by mathematical operators (addition *+*, subtraction *-*, multiplication *\**, division */*, exponentiation **********). + +[[syntax-boolean_expression]] +boolean_expression: A boolean expression consists of relations (*<*, *<=*, *=*, */=*, *>=*, *>*) between names and numbers combined by boolean operators (conjunction *and*, disjunction *or*). + +The type system is inspired by Ada, but differs in some details. In contrast to Ada, integer variables are considered type-compatible. Explicit type conversions of integer variables are neither required nor supported. + +Some parts of this document are marked by tags of the form [ §A-B-C ]. These tags are added for testing purposes and can be ignored by the reader. + +=== Scalar Types + +==== Integer Type + +An integer type is used to represent numbers. Two types of integers are supported: modular type and range type. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-modular_type]] +modular_type ::= *type* xref:syntax-name[name] *is* *mod* xref:syntax-modulus[modulus] +[[syntax-range_type]] +range_type ::= *type* xref:syntax-name[name] *is* *range* xref:syntax-first[first] *..* xref:syntax-last[last] *with Size =>* xref:syntax-number[number] +[[syntax-modulus]] +modulus ::= xref:syntax-mathematical_expression[mathematical_expression] +[[syntax-first]] +first ::= xref:syntax-mathematical_expression[mathematical_expression] +[[syntax-last]] +last ::= xref:syntax-mathematical_expression[mathematical_expression] +---- + +*Static Semantics* + +A modular type represents the values from 0 to one less than the xref:syntax-modulus[modulus]. The bit size of a modular type is determined by calculating the binary logarithm of xref:syntax-modulus[modulus]. + +The set of values of a range type consists of all numbers from the lower bound to the upper bound. For a range type the bit size has to be specified explicitly. + +*Example* + +[source,ada,rflx,basic_declaration] +---- +type Address is mod 2**48 +---- + +[source,ada,rflx,basic_declaration] +---- +type Type_Length is range 46 .. 2**16 - 1 with Size => 16 +---- + +==== Enumeration Type + +An enumeration type represents a value out of a list of possible values. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-enumeration_type]] +enumeration_type ::= *type* xref:syntax-name[name] *is* *(* xref:syntax-literals[literals] *)* *with* xref:syntax-enumeration_aspects[enumeration_aspects] +[[syntax-literals]] +literals ::= xref:syntax-literal[literal] { **,** xref:syntax-literal[literal] } +[[syntax-literal]] +literal ::= xref:syntax-name[name] [*=>* xref:syntax-number[number]] +[[syntax-enumeration_aspects]] +enumeration_aspects ::= xref:syntax-enumeration_aspect[enumeration_aspect] { **,** xref:syntax-enumeration_aspect[enumeration_aspect] } +[[syntax-enumeration_aspect]] +enumeration_aspect ::= xref:syntax-size_aspect[size_aspect] | xref:syntax-always_valid_aspect[always_valid_aspect] +[[syntax-always_valid_aspect]] +always_valid_aspect ::= *Always_Valid* [ *=>* ( *True* | *False* ) ] +---- + +*Static Semantics* + +The set of values of an enumeration type consists of the list of declared enumeration literals. Each enumeration literal has a distinct value. If no explicit value is given, the first literal is zero, and the value of each subsequent literal is incremented by one. Literals with and without explicit value must not be intermixed in one definition. The bit size of the enumeration type must be specified explicitly. Optionally, an enumeration type can be flagged as always valid. A message field with such type is always considered valid, whether or not its value corresponds to one of the specified literals. + +*Example* + +[source,ada,rflx,basic_declaration] +---- +type Tag is (Msg_Error, Msg_Data) with Size => 1 +---- + +[source,ada,rflx,basic_declaration] +---- +type Ether_Type is + (ET_IPv4 => 16#0800#, + ET_ARP => 16#0806#, + ET_VLAN_Tag => 16#8100#, + ET_IPv6 => 16#86DD#, + ET_VLAN_Tag_Double => 16#9100#) +with Size => 16, Always_Valid +---- + +==== Boolean + +`Boolean` is a built-in enumeration type with the literals `False => 0` and `True => 1` with a size of 1 bit. + +=== Message Type + +A message type is a collection components. Additional then clauses allow to define conditions and dependencies between components. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-message_type]] +message_type ::= + *type* xref:syntax-name[name] *is* + ( *message* + [ xref:syntax-null_component[null_component] ] + xref:syntax-component[component] + { xref:syntax-component[component] } + *end message* [ *with* + xref:syntax-message_aspects[message_aspects] ] + | *null message* ) +[[syntax-component]] +component ::= + xref:syntax-name[name] *:* type_xref:syntax-name[name] + [ *with* xref:syntax-aspects[aspects] ] + [ *if* xref:syntax-condition[condition] ] + { xref:syntax-then_clause[then_clause] } *;* +[[syntax-null_component]] +null_component ::= *null* xref:syntax-then_clause[then_clause] *;* +[[syntax-then_clause]] +then_clause ::= + *then* xref:syntax-component_name[component_name] + [ *with* xref:syntax-aspects[aspects] ] + [ *if* xref:syntax-condition[condition] ] +[[syntax-aspects]] +aspects ::= xref:syntax-aspect[aspect] { *,* xref:syntax-aspect[aspect] } +[[syntax-aspect]] +aspect ::= xref:syntax-first_aspect[first_aspect] | xref:syntax-size_aspect[size_aspect] +[[syntax-first_aspect]] +first_aspect ::= *First* *=>* xref:syntax-mathematical_expression[mathematical_expression] +[[syntax-size_aspect]] +size_aspect ::= *Size* *=>* xref:syntax-mathematical_expression[mathematical_expression] +[[syntax-condition]] +condition ::= xref:syntax-boolean_expression[boolean_expression] +[[syntax-message_aspects]] +message_aspects ::= xref:syntax-message_aspect[message_aspect] { *,* xref:syntax-message_aspect[message_aspect] } +[[syntax-message_aspect]] +message_aspect ::= xref:syntax-checksum_aspect[checksum_aspect] +[[syntax-checksum_aspect]] +checksum_aspect ::= *Checksum* *=>* *(* xref:syntax-checksum_definition[checksum_definition] { *,* xref:syntax-checksum_definition[checksum_definition] } *)* +[[syntax-checksum_definition]] +checksum_definition ::= xref:syntax-name[name] *=>* *(* xref:syntax-checksum_element[checksum_element] { *,* xref:syntax-checksum_element[checksum_element] } *)* +[[syntax-checksum_element]] +checksum_element ::= xref:syntax-name[name] | xref:syntax-name[name]*'Size* | xref:syntax-field_range[field_range] +[[syntax-field_range]] +field_range ::= xref:syntax-field_range_first[field_range_first] *..* xref:syntax-field_range_last[field_range_last] +[[syntax-field_range_first]] +field_range_first ::= xref:syntax-name[name]*'First* | xref:syntax-name[name]*'Last + 1* +[[syntax-field_range_last]] +field_range_last ::= xref:syntax-name[name]*'Last* | xref:syntax-name[name]*'First - 1* +---- + +*Static Semantics* + +A message type specifies the message format of a protocol. Each component corresponds to one field in a message. A then clause of a component allows to define which field follows. If no then clause is given, it is assumed that always the next component of the message follows. If no further component follows, it is assumed that the message ends with this field. The end of a message can also be denoted explicitly by adding a then clause to *null*. Optionally a then clause can contain a condition under which the corresponding field follows and aspects which allow to define the size of the next field and the location of its first bit. These aspects can also be specified in the component. Each aspect can be specified either in the component or in all incoming then clauses, but not in both. The condition can refer to previous fields (including the component containing the then clause). A condition can also be added to a component. A component condition is equivalent to adding a condition to all incoming then clauses. If a component condition as well as a condition at an incoming then clause exists, both conditions are combined by a logical conjunction. If required, a null component can be used to specify the size of the first field in the message. An empty message can be represented by a null message. + +The field type `Opaque` represents an unconstrained sequence of bytes. The size of opaque fields must be always defined by a size aspect. Opaque fields and sequence fields must be byte aligned. The size of a message must be a multiple of 8 bit. + +A checksum aspect specifies which parts of a message is covered by a checksum. The definition of the checksum calculation is not part of the specification. Code based on the message specification must provide a function which is able to verify a checksum using the specified checksum elements. A checksum element can be a field value, a field size or a range of fields. The point where a checksum should be checked during parsing or generated during serialization must be defined for each checksum. For this purpose the `Valid_Checksum` attribute is added to a condition. All message parts on which the checksum depends have to be known at this point. + +*Example* + +[source,ada,rflx,basic_declaration] +---- +type Frame is + message + Destination : Address; + Source : Address; + Type_Length_TPID : Type_Length + then TPID + with First => Type_Length_TPID'First + if Type_Length_TPID = 16#8100# + then Payload + with Size => Type_Length_TPID * 8 + if Type_Length_TPID <= 1500 + then Ether_Type + with First => Type_Length_TPID'First + if Type_Length_TPID >= 1536 and Type_Length_TPID /= 16#8100#; + TPID : TPID; + TCI : TCI; + Ether_Type : Ether_Type + then Payload + with Size => Message'Last - Ether_Type'Last; + Payload : Opaque + then null + if Payload'Size / 8 >= 46 and Payload'Size / 8 <= 1500; + end message +---- + +[source,ada,rflx,basic_declaration] +---- +type Empty_Message is null message +---- + +=== Type Refinement + +A type refinement describes the relation of a component in a message type to another message type. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-type_refinement]] +type_refinement ::= + *for* xref:syntax-refined_type_name[refined_type_name] *use* **( **refined_component_xref:syntax-name[name] **=>** xref:syntax-message_type_name[message_type_name] **)** + [ **if** xref:syntax-condition[condition] ] +[[syntax-refined_type_name]] +refined_type_name ::= xref:syntax-qualified_name[qualified_name] +[[syntax-message_type_name]] +message_type_name ::= xref:syntax-qualified_name[qualified_name] +[[syntax-qualified_name]] +qualified_name ::= xref:syntax-name[name] { **.** xref:syntax-name[name] } +[[syntax-condition]] +condition ::= xref:syntax-boolean_expression[boolean_expression] +---- + +*Static Semantics* + +A type refinement describes under which condition a specific protocol message can be expected inside of a payload field. Only components of type `Opaque` can be refined. Types defined in other packages are referenced by a qualified name in the form package_name.message_type_name. The condition can refer to components of the refined type. To indicate that a refined component is empty (i.e. does not exit) under a certain condition, a null message can be used as message type. + +*Example* + +[source,ada,rflx,basic_declaration] +---- +for Ethernet::Frame use (Payload => IPv4::Packet) + if Ether_Type = Ethernet::IPV4 +---- + +=== Type Derivation + +A type derivation allows to create a new message type based on an existing message type. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-type_derivation]] +type_derivation ::= *type* xref:syntax-name[name] *is new* xref:syntax-base_type_name[base_type_name] +[[syntax-base_type_name]] +base_type_name ::= xref:syntax-qualified_name[qualified_name] +---- + +*Static Semantics* + +A derived message type derives its specification from a base type. Type refinements of a base message type are not inherited by the derived message type. + +*Example* + +[source,ada,rflx,basic_declaration] +---- +type Specific_Extension is new Extension +---- + +=== Sequence Type + +A sequence type represents a list of similar elements. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-sequence_type]] +sequence_type ::= *type* xref:syntax-name[name] *is sequence of* element_type_xref:syntax-name[name] +---- + +*Static Semantics* + +A sequence consists of a number of elements with similar type. Scalar types as well as message types can be used as element type. When a sequence is used in a message type, its bit length has to be specified by a size aspect. + +*Example* + +[source,ada,rflx,basic_declaration] +---- +type Options is sequence of Option +---- + +=== Protocol Sessions [§S] + +A session defines the dynamic behavior of a protocol using a finite state machine. The external interface of a session is defined by parameters. The initial and final state is defined by aspects. The declaration part enables the declaration of session global variables. The main part of a session definition are the state definitions. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-session]] +session ::= + *generic* + { xref:syntax-session_parameter[session_parameter] } + *session* xref:syntax-name[name] *with* + *Initial =>* state_xref:syntax-name[name], + *Final =>* state_xref:syntax-name[name] + *is* + { xref:syntax-session_declaration[session_declaration] } + *begin* + { xref:syntax-state[state] } + *end* xref:syntax-name[name] +---- + +*Example* + +[source,ada,rflx,basic_declaration] +---- +generic + X : Channel with Readable, Writable; + type T is private; + with function F return T; + with function G (P : T) return Boolean; +session S with + Initial => A, + Final => B +is + Y : Boolean := False; +begin + state A + with Desc => "rfc1149.txt+51:4-52:9" + is + Z : Boolean := Y; + M : TLV::Message; + begin + X'Read (M); + transition + then B + with Desc => "rfc1149.txt+45:4-47:8" + if Z = True + and G (F) = True + then A + end A; + + state B is null state; +end S +---- + +==== Session Parameters [§S-P] + +Private types, functions and channels can be defined as session parameters. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-session_parameter]] +session_parameter ::= ( xref:syntax-private_type_declaration[private_type_declaration] | xref:syntax-function_declaration[function_declaration] | xref:syntax-channel_declaration[channel_declaration] ) *;* +---- + +===== Private Types [§S-P-P] + +A private type represents an externally defined type. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-private_type_declaration]] +private_type_declaration ::= *type* xref:syntax-name[name] *is private* +---- + +*Example* + +[source,ada,rflx,session_parameter] +---- +type Hash is private +---- + +===== Functions [§S-P-F] + +Functions enable the execution of externally defined code. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-function_declaration]] +function_declaration ::= *with function* xref:syntax-name[name] [ *(* xref:syntax-function_parameter[function_parameter] { **,** xref:syntax-function_parameter[function_parameter] } **)** ] +---- +[[syntax-function_parameter]] +function_parameter ::= parameter_xref:syntax-name[name] *:* type_xref:syntax-name[name] + +*Static Semantics* + +[%collapsible] +==== +Allowed parameter types [§S-P-F-P]: + +* Scalars [§S-P-F-P-S] +* Definite messages [§S-P-F-P-M] +* Opaque fields of messages [§S-P-F-P-O] + +Allowed return types [§S-P-F-R]: + +* Scalars [§S-P-F-R-S] +* Definite messages [§S-P-F-R-M] + +Definite messages are messages with no optional fields and a bounded size (i.e. all size aspects contain no reference to `Message`). +==== + +*SPARK* + +For each function declaration in the session specification a formal procedure declaration is added to the corresponding generic session package. The return type and parameters of a function are represented by the first and subsequent parameters of the generated procedure declaration. + +*Example* + +[source,ada,rflx,session_parameter] +---- +with function Decrypt (Key_Update_Message : Key_Update_Message; Sequence_Number : Sequence_Number; Encrypted_Record : Opaque) return TLS_Inner_Plaintext +---- + +===== Channels [§S-P-C] + +Channels provide a way for communicating with other systems using messages. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-channel_declaration]] +channel_declaration ::= xref:syntax-name[name] *: Channel with* xref:syntax-channel_aspect[channel_aspect] { *,* xref:syntax-channel_aspect[channel_aspect] } +[[syntax-channel_aspect]] +channel_aspect ::= *Readable* | *Writable* +---- + +*Static Semantics* + +Properties of channels: + +* Readable [§S-P-C-R] +* Writable [§S-P-C-W] +* Readable and writable [§S-P-C-RW] + +*Example* + +[source,ada,rflx,session_parameter] +---- +Data_Channel : Channel with Readable, Writable +---- + +==== Declarations [§S-D] + +Variables and renamings can be globally declared (i.e. for the scope of the complete session). + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-session_declaration]] +session_declaration ::= ( xref:syntax-variable_declaration[variable_declaration] | xref:syntax-renaming_declaration[renaming_declaration] ) **;** +---- + +===== Variable Declaration [§S-D-V] + +A declared variable must have a type and can be optionally initialized using an expression. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-variable_declaration]] +variable_declaration ::= variable_xref:syntax-name[name] *:* type_xref:syntax-name[name] [ *:=* initialization_xref:syntax-expression[expression] ] +---- + +*Static Semantics* + +[%collapsible] +==== +Types [§S-D-V-T]: + +* Scalar [§S-D-V-T-SC] +* Message [§S-D-V-T-M] +* Scalar Sequence [§S-D-V-T-SS] +* Message Sequence [§S-D-V-T-MS] + +Initialization expressions [§S-D-V-E]: + +* No initialization [§S-D-V-E-N] +* Mathematical Expressions [§S-D-V-E-ME] +* Literals [§S-D-V-E-L] +* Variables [§S-D-V-E-V] +* Message Aggregates [§S-D-V-E-MA] +* Aggregates [§S-D-V-E-A] +* Valid Attributes [§S-D-V-E-VAT] +* Opaque Attributes [§S-D-V-E-OAT] +* Head Attributes [§S-D-V-E-HAT] +* Has_Data Attributes [§S-D-V-E-HDAT] +* Selected Expressions [§S-D-V-E-S] +* List Comprehensions [§S-D-V-E-LC] +* Bindings [§S-D-V-E-B] +* Quantified Expressions [§S-D-V-E-Q] +* Calls [§S-D-V-E-CL] +* Conversions [§S-D-V-E-CV] +==== + +*Example* + +[source,ada,rflx,declaration] +---- +Error_Sent : Boolean := False +---- + +===== Renaming Declaration [§S-D-R] + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-renaming_declaration]] +renaming_declaration ::= xref:syntax-name[name] *:* message_type_xref:syntax-name[name] *renames* message_variable_xref:syntax-name[name] *.* field_xref:syntax-name[name] +---- + +*Example* + +[source,ada,rflx,declaration] +---- +Client_Hello_Message : TLS_Handshake::Client_Hello renames Client_Hello_Handshake_Message.Payload +---- + +==== States [§S-S] + +A state defines the to be executed actions and the transitions to subsequent states. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-state]] +state ::= + *state* xref:syntax-name[name] + [ *with* xref:syntax-description_aspect[description_aspect] ] + *is* + { xref:syntax-state_declaration[state_declaration] } + *begin* + { xref:syntax-state_action[state_action] } + *transition* + { xref:syntax-conditional_transition[conditional_transition] } + xref:syntax-transition[transition] + [ *exception* + xref:syntax-transition[transition] ] + *end* xref:syntax-name[name] + | *state* xref:syntax-name[name] *is null state* +[[syntax-description_aspect]] +description_aspect ::= *Desc =>* xref:syntax-string[string] +---- + +*Static Semantics* + +An § exception transition [§S-S-E] must be defined just in case any action might lead to a critical (potentially non-recoverable) error: + +* Insufficient memory for setting a field of a message +* Insufficient memory for appending an element to a sequence or extending a sequence by another sequence + +Exception transitions are currently also used for other cases. This behavior will change in the future (cf. https://github.com/Componolit/RecordFlux/issues/569[#569]). + +A § null state [§S-S-N] does not contain any actions or transitions, and represents the final state of a session state machine. + +*Dynamic Semantics* + +After entering a state the declarations and actions of the state are executed. If a non-recoverable error occurs, the execution is aborted and the state is changed based on the exception transition. When all action were executed successfully, the conditions of the transitions are checked in the given order. If a condition is fulfilled, the corresponding transition is taken to change the state. If no condition could be fulfilled or no conditional transitions were defined, the default transition is used. + +*Example* + +[source,ada,rflx,state] +---- +state A + with Desc => "rfc1149.txt+51:4-52:9" +is + Z : Boolean := Y; + M : TLV::Message; +begin + X'Read (M); +transition + then B + with Desc => "rfc1149.txt+45:4-47:8" + if Z = True and G (F) = True + then A +end A +---- + +[source,ada,rflx,state] +---- +state B is null state +---- + +===== State Declarations [§S-S-D] + +Variable declarations [§S-S-D-V] and § renaming declarations [§S-S-D-R] in a state have a state-local scope, i.e., local declarations cannot be accessed from other states. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-state_declaration]] +state_declaration ::= ( xref:syntax-variable_declaration[variable_declaration] | xref:syntax-renaming_declaration[renaming_declaration] ) *;* +---- + +*Static Semantics* + +A local declaration must not hide a global declaration. + +[%collapsible] +==== +Types [§S-S-D-V-T]: + +* Scalar [§S-S-D-V-T-SC] +* Message [§S-S-D-V-T-M] +* Scalar Sequence [§S-S-D-V-T-SS] +* Message Sequence [§S-S-D-V-T-MS] + +Initialization expressions [§S-S-D-V-E]: + +* No initialization [§S-S-D-V-E-N] +* Mathematical Expressions [§S-S-D-V-E-ME] +* Literals [§S-S-D-V-E-L] +* Variables [§S-S-D-V-E-V] +* Message Aggregates [§S-S-D-V-E-MA] +* Aggregates [§S-S-D-V-E-A] +* Valid Attributes [§S-S-D-V-E-VAT] +* Opaque Attributes [§S-S-D-V-E-OAT] +* Head Attributes [§S-S-D-V-E-HAT] +* Has_Data Attributes [§S-S-D-V-E-HDAT] +* Selected Expressions [§S-S-D-V-E-S] +* List Comprehensions [§S-S-D-V-E-LC] +* Bindings [§S-S-D-V-E-B] +* Quantified Expressions [§S-S-D-V-E-Q] +* Calls [§S-S-D-V-E-CL] +* Conversions [§S-S-D-V-E-CV] +==== + +===== State Transitions [§S-S-T] + +State transitions define the conditions for the change to subsequent states. An arbitrary number of conditional transitions can be defined. The last transition in a state definition is the default transition, which does not contain any condition. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-conditional_transition]] +conditional_transition ::= + xref:syntax-transition[transition] + *if* conditional_xref:syntax-expression[expression] +[[syntax-transition]] +transition ::= + *then* state_xref:syntax-name[name] + [ *with* xref:syntax-description_aspect[description_aspect] ] +---- + +*Static Semantics* + +[%collapsible] +==== +Condition expressions: + +* No condition [§S-S-T-N] +* Mathematical Expressions [§S-S-T-ME] +* Literals [§S-S-T-L] +* Variables [§S-S-T-V] +* Message Aggregates [§S-S-T-MA] +* Aggregates [§S-S-T-A] +* Valid Attributes [§S-S-T-VAT] +* Opaque Attributes [§S-S-T-OAT] +* Head Attributes [§S-S-T-HAT] +* Has_Data Attributes [§S-S-T-HDAT] +* Selected Expressions [§S-S-T-S] +* List Comprehensions [§S-S-T-LC] +* Bindings [§S-S-T-B] +* Quantified Expressions [§S-S-T-Q] +* Calls [§S-S-T-CL] +* Conversions [§S-S-T-CV] +==== + +*Example* + +[source,ada,rflx,conditional_transition] +---- +then B + with Desc => "rfc1149.txt+45:4-47:8" + if Z = True and G (F) = True +---- + +===== State Actions [§S-S-A] + +The state actions are executed after entering a state. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-state_action]] +state_action ::= ( xref:syntax-assignment[assignment] | xref:syntax-append[append] | xref:syntax-extend[extend] | xref:syntax-reset[reset] | xref:syntax-read[read] | xref:syntax-write[write] ) *;* +---- + +====== Assignment Statements [§S-S-A-A] + +An assignment sets the value of variable. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-assignment]] +assignment ::= variable_xref:syntax-name[name] *:=* xref:syntax-expression[expression] +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-S-A-A-ME] +* Literals [§S-S-A-A-L] +* Variables [§S-S-A-A-V] +* Message Aggregates [§S-S-A-A-MA] +* Aggregates [§S-S-A-A-A] +* Valid Attributes [§S-S-A-A-VAT] +* Opaque Attributes [§S-S-A-A-OAT] +* Head Attributes [§S-S-A-A-HAT] +* Has_Data Attributes [§S-S-A-A-HDAT] +* Selected Expressions [§S-S-A-A-S] +* List Comprehensions [§S-S-A-A-LC] +* Bindings [§S-S-A-A-B] +* Quantified Expressions [§S-S-A-A-Q] +* Calls [§S-S-A-A-CL] +* Conversions [§S-S-A-A-CV] +==== + +*Dynamic Semantics* + +An assignment always creates a copy of the original object. + +*Example* + +[source,ada,rflx,assignment_statement] +---- +Error_Sent := True +---- + +====== Append Attribute Statements [§S-S-A-AP] + +An element is added to the end of a sequence using the Append attribute. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-append]] +append ::= sequence_xref:syntax-name[name]*'Append (* xref:syntax-expression[expression] *)* +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-S-A-AP-ME] +* Literals [§S-S-A-AP-L] +* Variables [§S-S-A-AP-V] +* Message Aggregates [§S-S-A-AP-MA] +* Aggregates [§S-S-A-AP-A] +* Valid Attributes [§S-S-A-AP-VAT] +* Opaque Attributes [§S-S-A-AP-OAT] +* Head Attributes [§S-S-A-AP-HAT] +* Has_Data Attributes [§S-S-A-AP-HDAT] +* Selected Expressions [§S-S-A-AP-S] +* List Comprehensions [§S-S-A-AP-LC] +* Bindings [§S-S-A-AP-B] +* Quantified Expressions [§S-S-A-AP-Q] +* Calls [§S-S-A-AP-CL] +* Conversions [§S-S-A-AP-CV] +==== + +*Dynamic Semantics* + +Appending an element to a sequence might lead to an exception transition. + +*Example* + +[source,ada,rflx,attribute_statement] +---- +Parameter_Request_List'Append (DHCP::Domain_Name_Option) +---- + +====== Extend Attribute Statements [§S-S-A-EX] + +The Extend attributes adds a sequence of elements to the end of a sequence. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-extend]] +extend ::= sequence_xref:syntax-name[name]*'Extend (* xref:syntax-expression[expression] *)* +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-S-A-EX-ME] +* Literals [§S-S-A-EX-L] +* Variables [§S-S-A-EX-V] +* Message Aggregates [§S-S-A-EX-MA] +* Aggregates [§S-S-A-EX-A] +* Valid Attributes [§S-S-A-EX-VAT] +* Opaque Attributes [§S-S-A-EX-OAT] +* Head Attributes [§S-S-A-EX-HAT] +* Has_Data Attributes [§S-S-A-EX-HDAT] +* Selected Expressions [§S-S-A-EX-S] +* List Comprehensions [§S-S-A-EX-LC] +* Bindings [§S-S-A-EX-B] +* Quantified Expressions [§S-S-A-EX-Q] +* Calls [§S-S-A-EX-CL] +* Conversions [§S-S-A-EX-CV] +==== + +*Dynamic Semantics* + +Extending a sequence might lead to an exception transition. + +*Example* + +[source,ada,rflx,attribute_statement] +---- +Parameter_Request_List'Extend (Parameters) +---- + +====== Reset Attribute Statements [§S-S-A-RS] + +The state of a message or sequence can be cleared using the Reset attribute. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-reset]] +reset ::= xref:syntax-name[name]*'Reset* +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-S-A-RS-ME] +* Literals [§S-S-A-RS-L] +* Variables [§S-S-A-RS-V] +* Message Aggregates [§S-S-A-RS-MA] +* Aggregates [§S-S-A-RS-A] +* Valid Attributes [§S-S-A-RS-VAT] +* Opaque Attributes [§S-S-A-RS-OAT] +* Head Attributes [§S-S-A-RS-HAT] +* Has_Data Attributes [§S-S-A-RS-HDAT] +* Selected Expressions [§S-S-A-RS-S] +* List Comprehensions [§S-S-A-RS-LC] +* Bindings [§S-S-A-RS-B] +* Quantified Expressions [§S-S-A-RS-Q] +* Calls [§S-S-A-RS-CL] +* Conversions [§S-S-A-RS-CV] +==== + +*Dynamic Semantics* + +The existing state of a message or sequence is removed (and the corresponding buffer is cleared). + +*Example* + +[source,ada,rflx,attribute_statement] +---- +Message'Reset +---- + +====== Read Attribute Statements [§S-S-A-RD] + +The read attribute statement is used to retrieve a message from a channel. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-read]] +read ::= channel_xref:syntax-name[name]*'Read (* xref:syntax-expression[expression] *)* +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-S-A-RD-ME] +* Literals [§S-S-A-RD-L] +* Variables [§S-S-A-RD-V] +* Message Aggregates [§S-S-A-RD-MA] +* Aggregates [§S-S-A-RD-A] +* Valid Attributes [§S-S-A-RD-VAT] +* Opaque Attributes [§S-S-A-RD-OAT] +* Head Attributes [§S-S-A-RD-HAT] +* Has_Data Attributes [§S-S-A-RD-HDAT] +* Selected Expressions [§S-S-A-RD-S] +* List Comprehensions [§S-S-A-RD-LC] +* Bindings [§S-S-A-RD-B] +* Quantified Expressions [§S-S-A-RD-Q] +* Calls [§S-S-A-RD-CL] +* Conversions [§S-S-A-RD-CV] +==== + +*Example* + +[source,ada,rflx,attribute_statement] +---- +Data_Channel'Read (Message) +---- + +====== Write Attribute Statements [§S-S-A-WR] + +A message can be sent through a channel using a write attribute statement. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-write]] +write ::= channel_xref:syntax-name[name]*'Write (* xref:syntax-expression[expression] *)* +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-S-A-WR-ME] +* Literals [§S-S-A-WR-L] +* Variables [§S-S-A-WR-V] +* Message Aggregates [§S-S-A-WR-MA] +* Aggregates [§S-S-A-WR-A] +* Valid Attributes [§S-S-A-WR-VAT] +* Opaque Attributes [§S-S-A-WR-OAT] +* Head Attributes [§S-S-A-WR-HAT] +* Has_Data Attributes [§S-S-A-WR-HDAT] +* Selected Expressions [§S-S-A-WR-S] +* List Comprehensions [§S-S-A-WR-LC] +* Bindings [§S-S-A-WR-B] +* Quantified Expressions [§S-S-A-WR-Q] +* Calls [§S-S-A-WR-CL] +* Conversions [§S-S-A-WR-CV] +==== + +*Dynamic Semantics* + +Writing an invalid message leads to an exception transition. This behavior will change in the future (cf. https://github.com/Componolit/RecordFlux/issues/569[#569]). + +*Example* + +[source,ada,rflx,attribute_statement] +---- +Data_Channel'Write (Message) +---- + +==== Expressions [§S-E] + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-expression]] +expression ::= xref:syntax-literal[literal] | xref:syntax-variable[variable] | xref:syntax-mathematical_expression[mathematical_expression] | xref:syntax-boolean_expression[boolean_expression] | xref:syntax-message_aggregate[message_aggregate] | xref:syntax-aggregate[aggregate] | xref:syntax-attribute_reference[attribute_reference] | xref:syntax-selected[selected] | xref:syntax-comprehension[comprehension] | xref:syntax-binding[binding] | xref:syntax-quantified_expression[quantified_expression] | xref:syntax-call[call] | xref:syntax-conversion[conversion] +---- + +===== Literals + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-literal]] +literal ::= xref:syntax-name[name] | xref:syntax-number[number] +---- + +===== Variables + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-variable]] +variable ::= xref:syntax-name[name] +---- + +===== Message Aggregates + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-message_aggregate]] +message_aggregate ::= message_type_xref:syntax-name[name]*'(* xref:syntax-field_values[field_values] *)* +[[syntax-field_values]] +field_values ::= xref:syntax-field_value[field_value] { *,* xref:syntax-field_value[field_value] } | *null message* +[[syntax-field_value]] +field_value ::= field_xref:syntax-name[name] *=>* xref:syntax-expression[expression] +---- + +*Dynamic Semantics* + +An invalid condition during message creation leads to an exception transition. This behavior will change in the future (cf. https://github.com/Componolit/RecordFlux/issues/569[#569]). + +Insufficient memory during the message creation leads to an exception transition. + +*Example* + +[source,ada,rflx,extended_primary] +---- +TLS_Record::TLS_Record'(Tag => TLS_Record::Alert, Legacy_Record_Version => TLS_Record::TLS_1_2, Length => Alert_Message'Size / 8, Fragment => Alert_Message'Opaque) +---- + +[source,ada,rflx,extended_primary] +---- +Null_Message'(null message) +---- + +===== Aggregates [§S-E-A] + +An aggregate is a collection of elements. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-aggregate]] +aggregate ::= *[* xref:syntax-number[number] { *,* xref:syntax-number[number] } *]* +---- + +*Static Semantics* + +[%collapsible] +==== +All elements must be of the same type. + +Types [§S-E-A-T]: + +* Scalar [§S-E-A-T-SC] +* Message [§S-E-A-T-M] + +Expressions [§S-E-A-E]: + +* Mathematical Expressions [§S-E-A-E-ME] +* Literals [§S-E-A-E-L] +* Variables [§S-E-A-E-V] +* Message Aggregates [§S-E-A-E-MA] +* Aggregates [§S-E-A-E-A] +* Valid Attributes [§S-E-A-E-VAT] +* Opaque Attributes [§S-E-A-E-OAT] +* Head Attributes [§S-E-A-E-HAT] +* Has_Data Attributes [§S-E-A-E-HDAT] +* Selected Expressions [§S-E-A-E-S] +* List Comprehensions [§S-E-A-E-LC] +* Bindings [§S-E-A-E-B] +* Quantified Expressions [§S-E-A-E-Q] +* Calls [§S-E-A-E-CL] +* Conversions [§S-E-A-E-CV] +==== + +*Example* + +[source,ada,rflx,extended_primary] +---- +[0, 1, 2] +---- + +[source,ada,rflx,extended_primary] +---- +[] +---- + +===== Attribute Expressions [§S-E-AT] + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-attribute_reference]] +attribute_reference ::= xref:syntax-expression[expression]*'*xref:syntax-attribute_designator[attribute_designator] +[[syntax-attribute_designator]] +attribute_designator ::= *Valid* | *Opaque* | *Head* | *Has_Data* +---- + +*Static Semantics* + +The § Valid attribute [§S-E-AT-V] allows to determine the validity of a message or sequence. + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-E-AT-V-ME] +* Literals [§S-E-AT-V-L] +* Variables [§S-E-AT-V-V] +* Message Aggregates [§S-E-AT-V-MA] +* Aggregates [§S-E-AT-V-A] +* Valid Attributes [§S-E-AT-V-VAT] +* Opaque Attributes [§S-E-AT-V-OAT] +* Head Attributes [§S-E-AT-V-HAT] +* Has_Data Attributes [§S-E-AT-V-HDAT] +* Selected Expressions [§S-E-AT-V-S] +* List Comprehensions [§S-E-AT-V-LC] +* Bindings [§S-E-AT-V-B] +* Quantified Expressions [§S-E-AT-V-Q] +* Calls [§S-E-AT-V-CL] +* Conversions [§S-E-AT-V-CV] +==== + +The byte representation of a message can be retrieved using the § Opaque attribute [§S-E-AT-O]. + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-E-AT-O-ME] +* Literals [§S-E-AT-O-L] +* Variables [§S-E-AT-O-V] +* Message Aggregates [§S-E-AT-O-MA] +* Aggregates [§S-E-AT-O-A] +* Valid Attributes [§S-E-AT-O-VAT] +* Opaque Attributes [§S-E-AT-O-OAT] +* Head Attributes [§S-E-AT-O-HAT] +* Has_Data Attributes [§S-E-AT-O-HDAT] +* Selected Expressions [§S-E-AT-O-S] +* List Comprehensions [§S-E-AT-O-LC] +* Bindings [§S-E-AT-O-B] +* Quantified Expressions [§S-E-AT-O-Q] +* Calls [§S-E-AT-O-CL] +* Conversions [§S-E-AT-O-CV] +==== + +The § Head attribute [§S-E-AT-H] allows to get the first element of a sequence. + +[%collapsible] +==== +Prefix types: + +* Scalar Sequence [§S-E-AT-H-SS] +* Message Sequence [§S-E-AT-H-MS] + +Expressions: + +* Mathematical Expressions [§S-E-AT-H-ME] +* Literals [§S-E-AT-H-L] +* Variables [§S-E-AT-H-V] +* Message Aggregates [§S-E-AT-H-MA] +* Aggregates [§S-E-AT-H-A] +* Valid Attributes [§S-E-AT-H-VAT] +* Opaque Attributes [§S-E-AT-H-OAT] +* Head Attributes [§S-E-AT-H-HAT] +* Has_Data Attributes [§S-E-AT-H-HDAT] +* Selected Expressions [§S-E-AT-H-S] +* List Comprehensions [§S-E-AT-H-LC] +* Bindings [§S-E-AT-H-B] +* Quantified Expressions [§S-E-AT-H-Q] +* Calls [§S-E-AT-H-CL] +* Conversions [§S-E-AT-H-CV] +==== + +Whether a channel contains data can be checked with the § Has_Data attribute [§S-E-AT-HD]. + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-E-AT-HD-ME] +* Literals [§S-E-AT-HD-L] +* Variables [§S-E-AT-HD-V] +* Message Aggregates [§S-E-AT-HD-MA] +* Aggregates [§S-E-AT-HD-A] +* Valid Attributes [§S-E-AT-HD-VAT] +* Opaque Attributes [§S-E-AT-HD-OAT] +* Head Attributes [§S-E-AT-HD-HAT] +* Has_Data Attributes [§S-E-AT-HD-HDAT] +* Selected Expressions [§S-E-AT-HD-S] +* List Comprehensions [§S-E-AT-HD-LC] +* Bindings [§S-E-AT-HD-B] +* Quantified Expressions [§S-E-AT-HD-Q] +* Calls [§S-E-AT-HD-CL] +* Conversions [§S-E-AT-HD-CV] +==== + +*Dynamic Semantics* + +The use of the Opaque attribute on an invalid message or the use of the Head attribute on an empty sequence leads to an exception transition. This behavior will change in the future (cf. https://github.com/Componolit/RecordFlux/issues/569[#569]). + +*Example* + +[source,ada,rflx,extended_suffix] +---- +Message'Valid +---- + +===== Selected Expressions [§S-E-S] + +The Selected expression is used to get a value of a message field. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-selected]] +selected ::= message_xref:syntax-expression[expression] *.* field_xref:syntax-name[name] +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-E-S-ME] +* Literals [§S-E-S-L] +* Variables [§S-E-S-V] +* Message Aggregates [§S-E-S-MA] +* Aggregates [§S-E-S-A] +* Valid Attributes [§S-E-S-VAT] +* Opaque Attributes [§S-E-S-OAT] +* Head Attributes [§S-E-S-HAT] +* Has_Data Attributes [§S-E-S-HDAT] +* Selected Expressions [§S-E-S-S] +* List Comprehensions [§S-E-S-LC] +* Bindings [§S-E-S-B] +* Quantified Expressions [§S-E-S-Q] +* Calls [§S-E-S-CL] +* Conversions [§S-E-S-CV] +==== + +*Dynamic Semantics* + +An access to an invalid message field leads to an exception transition. This behavior will change in the future (cf. https://github.com/Componolit/RecordFlux/issues/569[#569]). + +*Example* + +[source,ada,rflx,extended_suffix] +---- +Ethernet_Frame.Payload +---- + +===== List Comprehensions [§S-E-LC] + +A list comprehension provides a way to create a new sequence based on an exisiting sequence. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-comprehension]] +comprehension ::= *[* *for* xref:syntax-name[name] *in* iterable_xref:syntax-expression[expression] *=>* selector_xref:syntax-expression[expression] *when* condition_xref:syntax-expression[expression] *]* +---- + +*Static Semantics* + +[%collapsible] +==== +* Source: Scalar sequence [§S-E-LC-SSS] +* Source: Message sequence [§S-E-LC-SMS] +* Source: Variable [§S-E-LC-V] +* Source: Selected [§S-E-LC-S] +* Target: Scalar sequence [§S-E-LC-TSS] +* Target: Message sequence [§S-E-LC-TMS] +* Condition: Selected [§S-E-LC-CS] +* Source sequence as target [§S-E-LC-SAT] +* Global declarations [§S-E-LC-GD] +* Local declarations [§S-E-LC-LD] +* State transitions [§S-E-LC-T] +* Assignment statements [§S-E-LC-A] +==== + +*Dynamic Semantics* + +An access to an invalid element in iterable__expression_ leads to an exception transition. This behavior will change in the future (cf. https://github.com/Componolit/RecordFlux/issues/569[#569]). + +*Example* + +[source,ada,rflx,extended_primary] +---- +[for O in Offer.Options => O.DHCP_Message_Type when O.Code = DHCP::DHCP_Message_Type_Option] +---- + +===== Bindings [§S-E-B] + +A binding can be used to name a subexpression and enables the use of a subexpression multiple times without the need for duplicating the expression or declaring a separate variable. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-binding]] +binding ::= + xref:syntax-expression[expression] + *where* + xref:syntax-name[name] *=* sub_xref:syntax-expression[expression] { *,* + xref:syntax-name[name] *=* sub_xref:syntax-expression[expression] } +---- + +*Static Semantics* + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-E-B-ME] +* Literals [§S-E-B-L] +* Variables [§S-E-B-V] +* Message Aggregates [§S-E-B-MA] +* Aggregates [§S-E-B-A] +* Valid Attributes [§S-E-B-VAT] +* Opaque Attributes [§S-E-B-OAT] +* Head Attributes [§S-E-B-HAT] +* Has_Data Attributes [§S-E-B-HDAT] +* Selected Expressions [§S-E-B-S] +* List Comprehensions [§S-E-B-LC] +* Bindings [§S-E-B-B] +* Quantified Expressions [§S-E-B-Q] +* Calls [§S-E-B-CL] +* Conversions [§S-E-B-CV] + +The type of the subexpression is inferred by the subexpression type and the expected type for all references of the name. +==== + +*Example* + +[source,ada,rflx,extended_suffix] +---- +TLS_Alert::Alert'(Level => Level, Description => Description) + where + Level = TLS_Alert::Fatal, + Description = GreenTLS_Alert_Message.Description +---- + +===== Quantified Expressions [§S-E-Q] + +Quantified expressions enable reasoning about properties of sequences. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-quantified_expression]] +quantified_expression ::= *for* xref:syntax-quantifier[quantifier] *in* iterable_xref:syntax-expression[expression] *=>* predicate_xref:syntax-expression[expression] +[[syntax-quantifier]] +quantifier ::= *all* | *some* +---- + +*Static Semantics* + +[%collapsible] +==== +Iterable expressions [§S-E-Q-I]: + +* Mathematical Expressions [§S-E-Q-I-ME] +* Literals [§S-E-Q-I-L] +* Variables [§S-E-Q-I-V] +* Message Aggregates [§S-E-Q-I-MA] +* Aggregates [§S-E-Q-I-A] +* Valid Attributes [§S-E-Q-I-VAT] +* Opaque Attributes [§S-E-Q-I-OAT] +* Head Attributes [§S-E-Q-I-HAT] +* Has_Data Attributes [§S-E-Q-I-HDAT] +* Selected Expressions [§S-E-Q-I-S] +* List Comprehensions [§S-E-Q-I-LC] +* Bindings [§S-E-Q-I-B] +* Quantified Expressions [§S-E-Q-I-Q] +* Calls [§S-E-Q-I-CL] +* Conversions [§S-E-Q-I-CV] + +Predicate expressions [§S-E-Q-P]: + +* Mathematical Expressions [§S-E-Q-P-ME] +* Literals [§S-E-Q-P-L] +* Variables [§S-E-Q-P-V] +* Message Aggregates [§S-E-Q-P-MA] +* Aggregates [§S-E-Q-P-A] +* Valid Attributes [§S-E-Q-P-VAT] +* Opaque Attributes [§S-E-Q-P-OAT] +* Head Attributes [§S-E-Q-P-HAT] +* Has_Data Attributes [§S-E-Q-P-HDAT] +* Selected Expressions [§S-E-Q-P-S] +* List Comprehensions [§S-E-Q-P-LC] +* Bindings [§S-E-Q-P-B] +* Quantified Expressions [§S-E-Q-P-Q] +* Calls [§S-E-Q-P-CL] +* Conversions [§S-E-Q-P-CV] +==== + +*Example* + +[source,ada,rflx,extended_primary] +---- +for all E in Server_Hello_Message.Extensions => E.Tag /= TLS_Handshake::ET_Supported_Versions +---- + +===== Calls [§S-E-CL] + +All functions which are declared in the session parameters can be called. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-call]] +call ::= xref:syntax-name[name] [ *(* argument_xref:syntax-expression[expression] { *,* argument_xref:syntax-expression[expression] } *)* ] +---- + +*Static Semantics* + +[%collapsible] +==== +Argument expressions: + +* No argument [§S-E-CL-N] +* Mathematical Expressions [§S-E-CL-ME] +* Literals [§S-E-CL-L] +* Variables [§S-E-CL-V] +* Message Aggregates [§S-E-CL-MA] +* Aggregates [§S-E-CL-A] +* Valid Attributes [§S-E-CL-VAT] +* Opaque Attributes [§S-E-CL-OAT] +* Head Attributes [§S-E-CL-HAT] +* Has_Data Attributes [§S-E-CL-HDAT] +* Selected Expressions [§S-E-CL-S] +* List Comprehensions [§S-E-CL-LC] +* Bindings [§S-E-CL-B] +* Quantified Expressions [§S-E-CL-Q] +* Calls [§S-E-CL-CL] +* Conversions [§S-E-CL-CV] +==== + +*Example* + +[source,ada,rflx,extended_primary] +---- +Decrypt (Key_Update_Message, Sequence_Number, TLS_Record_Message.Encrypted_Record) +---- + +===== Conversions [§S-E-CV] + +An opaque field of a message can be converted to a message. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-conversion]] +conversion ::= message_type_xref:syntax-name[name] *(* message_xref:syntax-expression[expression] *.* field_xref:syntax-name[name] *)* +---- + +*Static Semantics* + +A conversion is only allowed if a refinement for the message field and the intended target type exists. + +[%collapsible] +==== +Expressions: + +* Mathematical Expressions [§S-E-CV-ME] +* Literals [§S-E-CV-L] +* Variables [§S-E-CV-V] +* Message Aggregates [§S-E-CV-MA] +* Aggregates [§S-E-CV-A] +* Valid Attributes [§S-E-CV-VAT] +* Opaque Attributes [§S-E-CV-OAT] +* Head Attributes [§S-E-CV-HAT] +* Has_Data Attributes [§S-E-CV-HDAT] +* Selected Expressions [§S-E-CV-S] +* List Comprehensions [§S-E-CV-LC] +* Bindings [§S-E-CV-B] +* Quantified Expressions [§S-E-CV-Q] +* Calls [§S-E-CV-CL] +* Conversions [§S-E-CV-CV] +==== + +*Dynamic Semantics* + +An invalid condition of a refinement leads to an exception transition. This behavior will change in the future (cf. https://github.com/Componolit/RecordFlux/issues/569[#569]). + +*Example* + +[source,ada,rflx,extended_primary] +---- +Key_Update_Message (Handshake_Control_Message.Data) +---- + +=== Package + +A package is used to structure a specification. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-package]] +package ::= + *package* xref:syntax-name[name] *is* + { xref:syntax-basic_declaration[basic_declaration] } + *end* xref:syntax-name[name] *;* + +[[syntax-basic_declaration]] +basic_declaration := ( xref:syntax-modular_type[modular_type] | xref:syntax-range_type[range_type] | xref:syntax-enumeration_type[enumeration_type] | xref:syntax-message_type[message_type] | xref:syntax-type_refinement[type_refinement] | xref:syntax-session[session] ) *;* +---- + +*Static Semantics* + +A package is a collection of types and sessions. By convention one protocol is specified in one package. + +*Example* + +[source,ada,rflx] +---- +package Ethernet is + + type Address is mod 2**48; + type Type_Length is range 46 .. 2**16 - 1 with Size => 16; + type TPID is range 16#8100# .. 16#8100# with Size => 16; + type TCI is mod 2**16; + type Ether_Type is + (ET_IPv4 => 16#0800#, + ET_ARP => 16#0806#, + ET_VLAN_Tag => 16#8100#, + ET_IPv6 => 16#86DD#, + ET_VLAN_Tag_Double => 16#9100#) + with Size => 16, Always_Valid; + + type Frame is + message + Destination : Address; + Source : Address; + Type_Length_TPID : Type_Length + then TPID + with First => Type_Length_TPID'First + if Type_Length_TPID = 16#8100# + then Payload + with Size => Type_Length_TPID * 8 + if Type_Length_TPID <= 1500 + then Ether_Type + with First => Type_Length_TPID'First + if Type_Length_TPID >= 1536 and Type_Length_TPID /= 16#8100#; + TPID : TPID; + TCI : TCI; + Ether_Type : Ether_Type + then Payload + with Size => Message'Last - Ether_Type'Last; + Payload : Opaque + then null + if Payload'Size / 8 >= 46 and Payload'Size / 8 <= 1500; + end message; + +end Ethernet; +---- + +=== Context Clause + +The context clause is used to specify the relation to other packages and consists of a list of with clauses. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-context]] +context ::= { *with* xref:syntax-package[package]xref:syntax-name[name] *;* } +---- + +*Static Semantics* + +For each package referenced in a file, a corresponding with clause has to be added to the beginning of the file. + +*Example* + +[source,ada,rflx,context_clause] +---- +with Ethernet; +with IPv4; +---- + +=== File + +A RecordFlux specification file is recognized by the file extension `.rflx`. Each specification file contains exactly one package. The file name must match the package name in lower case characters. + +*Syntax* + +[subs="+macros,quotes"] +---- +[[syntax-file]] +file ::= + xref:syntax-context[context] + xref:syntax-package[package] +---- + +*Example* + +File: `in_ethernet.rflx` + +[source,ada,rflx,specification] +---- +with Ethernet; +with IPv4; + +package In_Ethernet is + + for Ethernet::Frame use (Payload => IPv4::Packet) + if Ether_Type = Ethernet::ET_IPv4; + +end In_Ethernet; +---- diff --git a/doc/Language-Reference.md b/doc/Language-Reference.md deleted file mode 100644 index 2564704f32..0000000000 --- a/doc/Language-Reference.md +++ /dev/null @@ -1,1410 +0,0 @@ -# Language Reference - -The specification language describes protocol message formats based on types. For each type of the specification language a description of its syntax and semantics and an example is given. A simple variant of Backus-Naur Form is used to describe the syntax. Reserved keywords and literals are marked in __bold__. Syntactic categories are highlighted by *italics*. To convey some semantic information the name of some syntactic categories are prefixed by a non-italicized part. Syntactic categories with non-italicized prefixes are equivalent to the category without the prefix. The following basic elements are used to describe the syntax of the language: - -*name*: A name consists of alphanumeric characters and underscores. By convention a name starts with a capital and after each underscore follows a capital as well (e.g., Mixed_Case_With_Underscores). - -*number*: A number consists of numerical digits. An underscore can be added between two digits to improve readability. - -*mathematical_expression*: A mathematical expression consists of numbers and names combined by mathematical operators (addition __+__, subtraction __-__, multiplication __\*__, division __/__, exponentiation __\*\*__). - -*boolean_expression*: A boolean expression consists of relations (__<__, __<=__, __=__, __/=__, __>=__, __>__) between names and numbers combined by boolean operators (conjunction __and__, disjunction __or__). - -The type system is inspired by Ada, but differs in some details. In contrast to Ada, integer variables are considered type-compatible. Explicit type conversions of integer variables are neither required nor supported. - -## Scalar Types - -### Integer Type - -An integer type is used to represent numbers. Two types of integers are supported: modular type and range type. - -#### Syntax - -*modular_type* ::= __type__ *name* __is__ __mod__ *modulus* __;__ - -*range_type* ::= __type__ *name* __is__ __range__ *first* __..__ *last* __with Size =>__ *number* __;__ - -*modulus* ::= *mathematical_expression* - -*first* ::= *mathematical_expression* - -*last* ::= *mathematical_expression* - -#### Static Semantics - -A modular type represents the values from 0 to one less than the *modulus*. The bit size of a modular type is determined by calculating the binary logarithm of *modulus*. - -The set of values of a range type consists of all numbers from the lower bound to the upper bound. For a range type the bit size has to be specified explicitly. - -#### Example - -```Ada RFLX basic_declaration -type Address is mod 2**48 -``` - -```Ada RFLX basic_declaration -type Type_Length is range 46 .. 2**16 - 1 with Size => 16 -``` - -### Enumeration Type - -An enumeration type represents a value out of a list of possible values. - -#### Syntax - -*enumeration_type* ::= __type__ *name* __is__ __(__ *literals* __)__ __with__ *enumeration_aspects* __;__ - -*literals* ::= *literal* { __,__ *literal* } - -*literal* ::= *name* [__=>__ *number*] - -*enumeration_aspects* ::= *enumeration_aspect* { __,__ *enumeration_aspect* } - -*enumeration_aspect* ::= *size_aspect* | *always_valid_aspect* - -*size_aspect* ::= __Size =>__ *number* - -*always_valid_aspect* ::= __Always_Valid__ [ __=>__ ( __True__ | __False__ ) ] - -#### Static Semantics - -The set of values of an enumeration type consists of the list of declared enumeration literals. Each enumeration literal has a distinct value. If no explicit value is given, the first literal is zero, and the value of each subsequent literal is incremented by one. Literals with and without explicit value must not be intermixed in one definition. The bit size of the enumeration type must be specified explicitly. Optionally, an enumeration type can be flagged as always valid. A message field with such type is always considered valid, whether or not its value corresponds to one of the specified literals. - -#### Example - -```Ada RFLX basic_declaration -type Tag is (Msg_Error, Msg_Data) with Size => 1 -``` - -```Ada RFLX basic_declaration -type Ether_Type is - (ET_IPv4 => 16#0800#, - ET_ARP => 16#0806#, - ET_VLAN_Tag => 16#8100#, - ET_IPv6 => 16#86DD#, - ET_VLAN_Tag_Double => 16#9100#) -with Size => 16, Always_Valid -``` - -### Boolean - -`Boolean` is a built-in enumeration type with the literals `False => 0` and `True => 1` with a size of 1 bit. - -## Message Type - -A message type is a collection components. Additional then clauses allow to define conditions and dependencies between components. - -#### Syntax - -*message_type* ::= __type__ *name* __is__ *message_definition* __;__ - -*message_definition* ::= __message__ [ *null_component* ] *component* { *component* } __end message__ [ __with__ *message_aspects* ] | __null message__ - -*component* ::= *component_name* __:__ *component_type* - [__with__ *aspects*] - [__if__ *condition*] - { *then_clause* } __;__ - -*null_component* ::= __null__ - *then_clause* __;__ - -*then_clause* ::= __then__ *component_name* - [__with__ *aspects*] - [__if__ *condition*] - -*component_name* ::= *name* | __null__ - -*component_type* ::= *name* - -*aspects* ::= *aspect* { __,__ *aspect* } - -*aspect* ::= *first_aspect* | *size_aspect* - -*first_aspect* ::= __First__ __=>__ *mathematical_expression* - -*size_aspect* ::= __Size__ __=>__ *mathematical_expression* - -*condition* ::= *boolean_expression* - -*message_aspects* ::= *message_aspect* { __,__ *message_aspect* } - -*message_aspect* ::= *checksum_aspect* - -*checksum_aspect* ::= __Checksum__ __=>__ (*checksum_definition* { __,__ *checksum_definition* }) - -*checksum_definition* ::= *name* __=>__ (*checksum_element* { __,__ *checksum_element* } - -*checksum_element* ::= *name* | *name* __'Size__ | *field_range* - -*field_range* ::= *field_range_first* __..__ *field_range_last* - -*field_range_first* ::= *name* __'First__ | *name* __'Last + 1__ - -*field_range_last* ::= *name* __'Last | *name* __'First - 1__ - -#### Static Semantics - -A message type specifies the message format of a protocol. Each component corresponds to one field in a message. A then clause of a component allows to define which field follows. If no then clause is given, it is assumed that always the next component of the message follows. If no further component follows, it is assumed that the message ends with this field. The end of a message can also be denoted explicitly by adding a then clause to __null__. Optionally a then clause can contain a condition under which the corresponding field follows and aspects which allow to define the size of the next field and the location of its first bit. These aspects can also be specified in the component. Each aspect can be specified either in the component or in all incoming then clauses, but not in both. The condition can refer to previous fields (including the component containing the then clause). A condition can also be added to a component. A component condition is equivalent to adding a condition to all incoming then clauses. If a component condition as well as a condition at an incoming then clause exists, both conditions are combined by a logical conjunction. If required, a null component can be used to specify the size of the first field in the message. An empty message can be represented by a null message. - -The field type `Opaque` represents an unconstrained sequence of bytes. The size of opaque fields must be always defined by a size aspect. Opaque fields and sequence fields must be byte aligned. The size of a message must be a multiple of 8 bit. - -A checksum aspect specifies which parts of a message is covered by a checksum. The definition of the checksum calculation is not part of the specification. Code based on the message specification must provide a function which is able to verify a checksum using the specified checksum elements. A checksum element can be a field value, a field size or a range of fields. The point where a checksum should be checked during parsing or generated during serialization must be defined for each checksum. For this purpose the `Valid_Checksum` attribute is added to a condition. All message parts on which the checksum depends have to be known at this point. - -#### Example - -```Ada RFLX basic_declaration -type Frame is - message - Destination : Address; - Source : Address; - Type_Length_TPID : Type_Length - then TPID - with First => Type_Length_TPID'First - if Type_Length_TPID = 16#8100# - then Payload - with Size => Type_Length_TPID * 8 - if Type_Length_TPID <= 1500 - then Ether_Type - with First => Type_Length_TPID'First - if Type_Length_TPID >= 1536 and Type_Length_TPID /= 16#8100#; - TPID : TPID; - TCI : TCI; - Ether_Type : Ether_Type - then Payload - with Size => Message'Last - Ether_Type'Last; - Payload : Opaque - then null - if Payload'Size / 8 >= 46 and Payload'Size / 8 <= 1500; - end message -``` - -```Ada RFLX basic_declaration -type Empty_Message is null message -``` - -## Type Refinement - -A type refinement describes the relation of a component in a message type to another message type. - -#### Syntax - -*type_refinement* ::= __for__ *refined_type_name* __use__ __(__ *refined_component_name* __=>__ *message_type_name* __)__ [ __if__ *condition* ] __;__ - -*refined_type_name* ::= *qualified_name* - -*refined_component_name* ::= *name* - -*message_type_name* ::= *qualified_name* - -*qualified_name* ::= *name* { __.__ *name* } - -*condition* ::= *boolean_expression* - -#### Static Semantics - -A type refinement describes under which condition a specific protocol message can be expected inside of a payload field. Only components of type `Opaque` can be refined. Types defined in other packages are referenced by a qualified name in the form package_name.message_type_name. The condition can refer to components of the refined type. To indicate that a refined component is empty (i.e. does not exit) under a certain condition, a null message can be used as message type. - -#### Example - -```Ada RFLX basic_declaration -for Ethernet::Frame use (Payload => IPv4::Packet) - if Ether_Type = Ethernet::IPV4 -``` - -## Type Derivation - -A type derivation allows to create a new message type based on an existing message type. - -#### Syntax - -*type_derivation* ::= __type__ *name* __is new__ *base_type_name*__;__ - -*base_type_name* ::= *qualified_name* - -#### Static Semantics - -A derived message type derives its specification from a base type. Type refinements of a base message type are not inherited by the derived message type. - -#### Example - -```Ada RFLX basic_declaration -type Specific_Extension is new Extension -``` - -## Sequence Type - -A sequence type represents a list of similar elements. - -#### Syntax - -*sequence_type* ::= __type__ *name* __is sequence of__ *element_type* __;__ - -*element_type* ::= *name* - -#### Static Semantics - -A sequence consists of a number of elements with similar type. Scalar types as well as message types can be used as element type. When a sequence is used in a message type, its bit length has to be specified by a size aspect. - -#### Example - -```Ada RFLX basic_declaration -type Options is sequence of Option -``` - -## Protocol Sessions [§S] - -A session defines the dynamic behavior of a protocol using a finite state machine. The external interface of a session is defined by parameters. The initial and final state is defined by aspects. The declaration part enables the declaration of session global variables. The main part of a session definition are the state definitions. - -__Syntax__ - -*session* ::= - __generic__ - { *session_parameter* } - __session__ *name* __with__ - __Initial =>__ state_*name*__,__ - __Final =>__ state_*name* - __is__ - { *session_declaration* } - __begin__ - { *state* } - __end__ *name*__;__ - -__Example__ - -```Ada RFLX basic_declaration -generic - X : Channel with Readable, Writable; - type T is private; - with function F return T; - with function G (P : T) return Boolean; -session S with - Initial => A, - Final => B -is - Y : Boolean := False; -begin - state A - with Desc => "rfc1149.txt+51:4-52:9" - is - Z : Boolean := Y; - M : TLV::Message; - begin - X'Read (M); - transition - then B - with Desc => "rfc1149.txt+45:4-47:8" - if Z = True - and G (F) = True - then A - end A; - - state B is null state; -end S -``` - -### Session Parameters [§S-P] - -Private types, functions and channels can be defined as session parameters. - -__Syntax__ - -*session_parameter* ::= *private_type_declaration* | *function_declaration* | *channel_declaration* - -#### Private Types [§S-P-P] - -A private type represents an externally defined type. - -__Syntax__ - -*private_type_declaration* ::= __type__ *name* __is private;__ - -__Static Semantics__ - -TBD - -__Example__ - -```Ada RFLX session_parameter -type Hash is private -``` - -#### Functions [§S-P-F] - -Functions enable the execution of externally defined code. - -__Syntax__ - -*function_declaration* ::= __with function__ *name* [ __(__ *function_parameter* { __,__ *function_parameter* } __)__ ] __;__ - -*function_parameter* ::= parameter_*name* __:__ type_*name* - -__Static Semantics__ - -Allowed parameter types [§S-P-F-P]: - -- Scalars [§S-P-F-P-S] -- Definite messages [§S-P-F-P-M] -- Opaque fields of messages [§S-P-F-P-O] - -Allowed return types [§S-P-F-R]: - -- Scalars [§S-P-F-R-S] -- Definite messages [§S-P-F-R-M] - -Definite messages are messages with no optional fields and a bounded size (i.e. all size aspects contain no reference to `Message`). - -__SPARK__ - -For each function declaration in the session specification a formal procedure declaration is added to the corresponding generic session package. The return type and parameters of a function are represented by the first and subsequent parameters of the generated procedure declaration. - -__Example__ - -```Ada RFLX session_parameter -with function Decrypt (Key_Update_Message : Key_Update_Message; Sequence_Number : Sequence_Number; Encrypted_Record : Opaque) return TLS_Inner_Plaintext -``` - -#### Channels [§S-P-C] - -Channels provide a way for communicating with other systems using messages. - -__Syntax__ - -*channel_declaration* ::= *name* __: Channel with__ *channel_aspects*__;__ - -*channel_aspects* ::= *channel_aspect* { __,__ *channel_aspect* } - -*channel_aspect* ::= __Readable__ | __Writable__ - -__Static Semantics__ - -Properties of channels: - -- Readable [§S-P-C-R] -- Writable [§S-P-C-W] -- Readable and writable [§S-P-C-RW] - -__Example__ - -```Ada RFLX session_parameter -Data_Channel : Channel with Readable, Writable -``` - -### Declarations [§S-D] - -Variables and renamings can be globally declared (i.e. for the scope of the complete session). - -__Syntax__ - -*session_declaration* ::= *variable_declaration* | *renaming_declaration* - -#### Variable Declaration [§S-D-V] - -A declared variable must have a type and can be optionally initialized using an expression. - -__Syntax__ - -*variable_declaration* ::= variable_*name* __:__ type_*name* [ __:=__ initialization_*expression* ] __;__ - -__Static Semantics__ - -
-Types [§S-D-V-T]: - -- Scalar [§S-D-V-T-SC] -- Message [§S-D-V-T-M] -- Scalar Sequence [§S-D-V-T-SS] -- Message Sequence [§S-D-V-T-MS] - -Initialization expressions [§S-D-V-E]: - -- No initialization [§S-D-V-E-N] -- Mathematical Expressions [§S-D-V-E-ME] -- Literals [§S-D-V-E-L] -- Variables [§S-D-V-E-V] -- Message Aggregates [§S-D-V-E-MA] -- Aggregates [§S-D-V-E-A] -- Valid Attributes [§S-D-V-E-VAT] -- Opaque Attributes [§S-D-V-E-OAT] -- Head Attributes [§S-D-V-E-HAT] -- Has_Data Attributes [§S-D-V-E-HDAT] -- Selected Expressions [§S-D-V-E-S] -- List Comprehensions [§S-D-V-E-LC] -- Bindings [§S-D-V-E-B] -- Quantified Expressions [§S-D-V-E-Q] -- Calls [§S-D-V-E-CL] -- Conversions [§S-D-V-E-CV] -
- -__Example__ - -```Ada RFLX declaration -Error_Sent : Boolean := False -``` - -#### Renaming Declaration [§S-D-R] - -TBD - -__Syntax__ - -*renaming_declaration* ::= *name* __:__ message_type_*name* __renames__ message_variable_*name* __.__ field_*name* __;__ - -__Static Semantics__ - -TBD - -__Example__ - -```Ada RFLX declaration -Client_Hello_Message : TLS_Handshake::Client_Hello renames Client_Hello_Handshake_Message.Payload -``` - -### States [§S-S] - -A state defines the to be executed actions and the transitions to subsequent states. - -__Syntax__ - -*state* ::= - __state__ *name* - [ __with__ *description_aspect* ] - __is__ - { *state_declaration* } - __begin__ - { *state_action* } - __transition__ - { *conditional_transition* } - *transition* - [ __exception__ - *transition* ] - __end__ *name*__;__ - | __state__ *name* __is null state;__ - -*description_aspect* ::= __Desc =>__ *string* - -__Static Semantics__ - -An § exception transition [§S-S-E] must be defined just in case any action might lead to a critical (potentially non-recoverable) error: - -- Insufficient memory for setting a field of a message -- Insufficient memory for appending an element to a sequence or extending a sequence by another sequence - -Exception transitions are currently also used for other cases. This behavior will change in the future (cf. [#569](https://github.com/Componolit/RecordFlux/issues/569)). - -A § null state [§S-S-N] does not contain any actions or transitions, and represents the final state of a session state machine. - -__Dynamic Semantics__ - -After entering a state the declarations and actions of the state are executed. If a non-recoverable error occurs, the execution is aborted and the state is changed based on the exception transition. When all action were executed successfully, the conditions of the transitions are checked in the given order. If a condition is fulfilled, the corresponding transition is taken to change the state. If no condition could be fulfilled or no conditional transitions were defined, the default transition is used. - -__Example__ - -```Ada RFLX state -state A - with Desc => "rfc1149.txt+51:4-52:9" -is - Z : Boolean := Y; - M : TLV::Message; -begin - X'Read (M); -transition - then B - with Desc => "rfc1149.txt+45:4-47:8" - if Z = True and G (F) = True - then A -end A -``` - -```Ada RFLX state -state B is null state -``` - -#### State Declarations [§S-S-D] - -Variable declarations [§S-S-D-V] and § renaming declarations [§S-S-D-R] in a state have a state-local scope, i.e., local declarations cannot be accessed from other states. - -__Syntax__ - -*state_declaration* ::= *variable_declaration* | *renaming_declaration* - -__Static Semantics__ - -
-A local declaration must not hide a global declaration. - -Types [§S-S-D-V-T]: - -- Scalar [§S-S-D-V-T-SC] -- Message [§S-S-D-V-T-M] -- Scalar Sequence [§S-S-D-V-T-SS] -- Message Sequence [§S-S-D-V-T-MS] - -Initialization expressions [§S-S-D-V-E]: - -- No initialization [§S-S-D-V-E-N] -- Mathematical Expressions [§S-S-D-V-E-ME] -- Literals [§S-S-D-V-E-L] -- Variables [§S-S-D-V-E-V] -- Message Aggregates [§S-S-D-V-E-MA] -- Aggregates [§S-S-D-V-E-A] -- Valid Attributes [§S-S-D-V-E-VAT] -- Opaque Attributes [§S-S-D-V-E-OAT] -- Head Attributes [§S-S-D-V-E-HAT] -- Has_Data Attributes [§S-S-D-V-E-HDAT] -- Selected Expressions [§S-S-D-V-E-S] -- List Comprehensions [§S-S-D-V-E-LC] -- Bindings [§S-S-D-V-E-B] -- Quantified Expressions [§S-S-D-V-E-Q] -- Calls [§S-S-D-V-E-CL] -- Conversions [§S-S-D-V-E-CV] -
- -#### State Transitions [§S-S-T] - -State transitions define the conditions for the change to subsequent states. An arbitrary number of conditional transitions can be defined. The last transition in a state definition is the default transition, which does not contain any condition. - -__Syntax__ - -*conditional_transition* ::= - *transition* - [ __with__ *description_aspect* ] - __if__ *expression* - -*transition* ::= - __then__ *state_name* - [ __with__ *description_aspect* ] - -__Static Semantics__ - -
-Condition expressions: - -- No condition [§S-S-T-N] -- Mathematical Expressions [§S-S-T-ME] -- Literals [§S-S-T-L] -- Variables [§S-S-T-V] -- Message Aggregates [§S-S-T-MA] -- Aggregates [§S-S-T-A] -- Valid Attributes [§S-S-T-VAT] -- Opaque Attributes [§S-S-T-OAT] -- Head Attributes [§S-S-T-HAT] -- Has_Data Attributes [§S-S-T-HDAT] -- Selected Expressions [§S-S-T-S] -- List Comprehensions [§S-S-T-LC] -- Bindings [§S-S-T-B] -- Quantified Expressions [§S-S-T-Q] -- Calls [§S-S-T-CL] -- Conversions [§S-S-T-CV] -
- -__Example__ - -```Ada RFLX conditional_transition -then B - with Desc => "rfc1149.txt+45:4-47:8" - if Z = True and G (F) = True -``` - -#### State Actions [§S-S-A] - -The state actions are executed after entering a state. - -__Syntax__ - -*state_action* ::= *assignment* | *append* | *extend* | *reset* | *read* | *write* - -##### Assignment Statements [§S-S-A-A] - -An assignment sets the value of variable. - -__Syntax__ - -*assignment* ::= *variable_name* __:=__ *expression*__;__ - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-S-A-A-ME] -- Literals [§S-S-A-A-L] -- Variables [§S-S-A-A-V] -- Message Aggregates [§S-S-A-A-MA] -- Aggregates [§S-S-A-A-A] -- Valid Attributes [§S-S-A-A-VAT] -- Opaque Attributes [§S-S-A-A-OAT] -- Head Attributes [§S-S-A-A-HAT] -- Has_Data Attributes [§S-S-A-A-HDAT] -- Selected Expressions [§S-S-A-A-S] -- List Comprehensions [§S-S-A-A-LC] -- Bindings [§S-S-A-A-B] -- Quantified Expressions [§S-S-A-A-Q] -- Calls [§S-S-A-A-CL] -- Conversions [§S-S-A-A-CV] -
- -__Dynamic Semantics__ - -An assignment always creates a copy of the original object. - -__Example__ - -```Ada RFLX assignment_statement -Error_Sent := True -``` - -##### Append Attribute Statements [§S-S-A-AP] - -An element is added to the end of a sequence using the Append attribute. - -__Syntax__ - -*append* ::= sequence_*name*__'Append (__*expression*__);__ - -__Dynamic Semantics__ - -Appending an element to a sequence might lead to an exception transition. - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-S-A-AP-ME] -- Literals [§S-S-A-AP-L] -- Variables [§S-S-A-AP-V] -- Message Aggregates [§S-S-A-AP-MA] -- Aggregates [§S-S-A-AP-A] -- Valid Attributes [§S-S-A-AP-VAT] -- Opaque Attributes [§S-S-A-AP-OAT] -- Head Attributes [§S-S-A-AP-HAT] -- Has_Data Attributes [§S-S-A-AP-HDAT] -- Selected Expressions [§S-S-A-AP-S] -- List Comprehensions [§S-S-A-AP-LC] -- Bindings [§S-S-A-AP-B] -- Quantified Expressions [§S-S-A-AP-Q] -- Calls [§S-S-A-AP-CL] -- Conversions [§S-S-A-AP-CV] -
- -__Example__ - -```Ada RFLX attribute_statement -Parameter_Request_List'Append (DHCP::Domain_Name_Option) -``` - -##### Extend Attribute Statements [§S-S-A-EX] - -The Extend attributes adds a sequence of elements to the end of a sequence. - -__Syntax__ - -*extend* ::= sequence_*name*__'Extend (__*expression*__);__ - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-S-A-EX-ME] -- Literals [§S-S-A-EX-L] -- Variables [§S-S-A-EX-V] -- Message Aggregates [§S-S-A-EX-MA] -- Aggregates [§S-S-A-EX-A] -- Valid Attributes [§S-S-A-EX-VAT] -- Opaque Attributes [§S-S-A-EX-OAT] -- Head Attributes [§S-S-A-EX-HAT] -- Has_Data Attributes [§S-S-A-EX-HDAT] -- Selected Expressions [§S-S-A-EX-S] -- List Comprehensions [§S-S-A-EX-LC] -- Bindings [§S-S-A-EX-B] -- Quantified Expressions [§S-S-A-EX-Q] -- Calls [§S-S-A-EX-CL] -- Conversions [§S-S-A-EX-CV] -
- -__Dynamic Semantics__ - -Extending a sequence might lead to an exception transition. - -__Example__ - -```Ada RFLX attribute_statement -Parameter_Request_List'Extend (Parameters) -``` - -##### Reset Attribute Statements [§S-S-A-RS] - -The state of a message or sequence can be cleared using the Reset attribute. - -__Syntax__ - -*reset* ::= message_*name*__'Reset (__*expression*__);__ - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-S-A-RS-ME] -- Literals [§S-S-A-RS-L] -- Variables [§S-S-A-RS-V] -- Message Aggregates [§S-S-A-RS-MA] -- Aggregates [§S-S-A-RS-A] -- Valid Attributes [§S-S-A-RS-VAT] -- Opaque Attributes [§S-S-A-RS-OAT] -- Head Attributes [§S-S-A-RS-HAT] -- Has_Data Attributes [§S-S-A-RS-HDAT] -- Selected Expressions [§S-S-A-RS-S] -- List Comprehensions [§S-S-A-RS-LC] -- Bindings [§S-S-A-RS-B] -- Quantified Expressions [§S-S-A-RS-Q] -- Calls [§S-S-A-RS-CL] -- Conversions [§S-S-A-RS-CV] -
- -__Dynamic Semantics__ - -The existing state of a message or sequence is removed (and the corresponding buffer is cleared). - -__Example__ - -```Ada RFLX attribute_statement -Message'Reset -``` - -##### Read Attribute Statements [§S-S-A-RD] - -The read attribute statement is used to retrieve a message from a channel. - -__Syntax__ - -*read* ::= channel_*name*__'Read (__*expression*__);__ - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-S-A-RD-ME] -- Literals [§S-S-A-RD-L] -- Variables [§S-S-A-RD-V] -- Message Aggregates [§S-S-A-RD-MA] -- Aggregates [§S-S-A-RD-A] -- Valid Attributes [§S-S-A-RD-VAT] -- Opaque Attributes [§S-S-A-RD-OAT] -- Head Attributes [§S-S-A-RD-HAT] -- Has_Data Attributes [§S-S-A-RD-HDAT] -- Selected Expressions [§S-S-A-RD-S] -- List Comprehensions [§S-S-A-RD-LC] -- Bindings [§S-S-A-RD-B] -- Quantified Expressions [§S-S-A-RD-Q] -- Calls [§S-S-A-RD-CL] -- Conversions [§S-S-A-RD-CV] -
- -__Example__ - -```Ada RFLX attribute_statement -Data_Channel'Read (Message) -``` - -##### Write Attribute Statements [§S-S-A-WR] - -A message can be sent through a channel using a write attribute statement. - -__Syntax__ - -*write* ::= channel_*name*__'Write (__*expression*__);__ - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-S-A-WR-ME] -- Literals [§S-S-A-WR-L] -- Variables [§S-S-A-WR-V] -- Message Aggregates [§S-S-A-WR-MA] -- Aggregates [§S-S-A-WR-A] -- Valid Attributes [§S-S-A-WR-VAT] -- Opaque Attributes [§S-S-A-WR-OAT] -- Head Attributes [§S-S-A-WR-HAT] -- Has_Data Attributes [§S-S-A-WR-HDAT] -- Selected Expressions [§S-S-A-WR-S] -- List Comprehensions [§S-S-A-WR-LC] -- Bindings [§S-S-A-WR-B] -- Quantified Expressions [§S-S-A-WR-Q] -- Calls [§S-S-A-WR-CL] -- Conversions [§S-S-A-WR-CV] -
- -__Dynamic Semantics__ - -Writing an invalid message leads to an exception transition. This behavior will change in the future (cf. [#569](https://github.com/Componolit/RecordFlux/issues/569)). - -__Example__ - -```Ada RFLX attribute_statement -Data_Channel'Write (Message) -``` - -### Expressions [§S-E] - -__Syntax__ - -*expression* ::= *literal* | *variable* | *mathematical_expression* | *message_aggregate* | *aggregate* | *attribute_reference* | *selected* | *comprehension* | *binding* | *quantified_expression* | *call* | *conversion* - -#### Literals - -__Syntax__ - -*literal* ::= *name* - -#### Variables - -__Syntax__ - -*variable* ::= *name* - -#### Message Aggregates - -__Syntax__ - -*message_aggregate* ::= message_type_*name*__'(__*field_values*__);__ - -*field_values* ::= *field_value* { __,__ *field_value* } | __null message__ - -*field_value* ::= *field_name* __=>__ *expression* - -__Dynamic Semantics__ - -An invalid condition during message creation leads to an exception transition. This behavior will change in the future (cf. [#569](https://github.com/Componolit/RecordFlux/issues/569)). - -Insufficient memory during the message creation leads to an exception transition. - -__Example__ - -```Ada RFLX extended_primary -TLS_Record::TLS_Record'(Tag => TLS_Record::Alert, Legacy_Record_Version => TLS_Record::TLS_1_2, Length => Alert_Message'Size / 8, Fragment => Alert_Message'Opaque) -``` - -```Ada RFLX extended_primary -Null_Message'(null message) -``` - -#### Aggregates [§S-E-A] - -__Syntax__ - -*aggregate* ::= __[__ [ *expression* { __,__ *expression* } ] __]__ - -__Static Semantics__ - -
-All elements must be of the same type. - -Types [§S-E-A-T]: - -- Scalar [§S-E-A-T-SC] -- Message [§S-E-A-T-M] - -Expressions [§S-E-A-E]: - -- Mathematical Expressions [§S-E-A-E-ME] -- Literals [§S-E-A-E-L] -- Variables [§S-E-A-E-V] -- Message Aggregates [§S-E-A-E-MA] -- Aggregates [§S-E-A-E-A] -- Valid Attributes [§S-E-A-E-VAT] -- Opaque Attributes [§S-E-A-E-OAT] -- Head Attributes [§S-E-A-E-HAT] -- Has_Data Attributes [§S-E-A-E-HDAT] -- Selected Expressions [§S-E-A-E-S] -- List Comprehensions [§S-E-A-E-LC] -- Bindings [§S-E-A-E-B] -- Quantified Expressions [§S-E-A-E-Q] -- Calls [§S-E-A-E-CL] -- Conversions [§S-E-A-E-CV] -
- -__Example__ - -```Ada RFLX extended_primary -[0, 1, 2] -``` - -```Ada RFLX extended_primary -[] -``` - -#### Attribute Expressions [§S-E-AT] - -__Syntax__ - -*attribute_reference* ::= *expression*__'__*attribute_designator* - -*attribute_designator* ::= __Valid__ | __Opaque__ | __Head__ | __Has_Data__ - -__Static Semantics__ - -The § Valid attribute [§S-E-AT-V] allows to determine the validity of a message or sequence. - -
-Expressions: - -- Mathematical Expressions [§S-E-AT-V-ME] -- Literals [§S-E-AT-V-L] -- Variables [§S-E-AT-V-V] -- Message Aggregates [§S-E-AT-V-MA] -- Aggregates [§S-E-AT-V-A] -- Valid Attributes [§S-E-AT-V-VAT] -- Opaque Attributes [§S-E-AT-V-OAT] -- Head Attributes [§S-E-AT-V-HAT] -- Has_Data Attributes [§S-E-AT-V-HDAT] -- Selected Expressions [§S-E-AT-V-S] -- List Comprehensions [§S-E-AT-V-LC] -- Bindings [§S-E-AT-V-B] -- Quantified Expressions [§S-E-AT-V-Q] -- Calls [§S-E-AT-V-CL] -- Conversions [§S-E-AT-V-CV] -
- -The byte representation of a message can be retrieved using the § Opaque attribute [§S-E-AT-O]. - -
-Expressions: - -- Mathematical Expressions [§S-E-AT-O-ME] -- Literals [§S-E-AT-O-L] -- Variables [§S-E-AT-O-V] -- Message Aggregates [§S-E-AT-O-MA] -- Aggregates [§S-E-AT-O-A] -- Valid Attributes [§S-E-AT-O-VAT] -- Opaque Attributes [§S-E-AT-O-OAT] -- Head Attributes [§S-E-AT-O-HAT] -- Has_Data Attributes [§S-E-AT-O-HDAT] -- Selected Expressions [§S-E-AT-O-S] -- List Comprehensions [§S-E-AT-O-LC] -- Bindings [§S-E-AT-O-B] -- Quantified Expressions [§S-E-AT-O-Q] -- Calls [§S-E-AT-O-CL] -- Conversions [§S-E-AT-O-CV] -
- -The § Head attribute [§S-E-AT-H] allows to get the first element of a sequence. - -
-Prefix types: - -- Scalar Sequence [§S-E-AT-H-SS] -- Message Sequence [§S-E-AT-H-MS] - -Expressions: - -- Mathematical Expressions [§S-E-AT-H-ME] -- Literals [§S-E-AT-H-L] -- Variables [§S-E-AT-H-V] -- Message Aggregates [§S-E-AT-H-MA] -- Aggregates [§S-E-AT-H-A] -- Valid Attributes [§S-E-AT-H-VAT] -- Opaque Attributes [§S-E-AT-H-OAT] -- Head Attributes [§S-E-AT-H-HAT] -- Has_Data Attributes [§S-E-AT-H-HDAT] -- Selected Expressions [§S-E-AT-H-S] -- List Comprehensions [§S-E-AT-H-LC] -- Bindings [§S-E-AT-H-B] -- Quantified Expressions [§S-E-AT-H-Q] -- Calls [§S-E-AT-H-CL] -- Conversions [§S-E-AT-H-CV] -
- -Whether a channel contains data can be checked with the § Has_Data attribute [§S-E-AT-HD]. - -
-Expressions: - -- Mathematical Expressions [§S-E-AT-HD-ME] -- Literals [§S-E-AT-HD-L] -- Variables [§S-E-AT-HD-V] -- Message Aggregates [§S-E-AT-HD-MA] -- Aggregates [§S-E-AT-HD-A] -- Valid Attributes [§S-E-AT-HD-VAT] -- Opaque Attributes [§S-E-AT-HD-OAT] -- Head Attributes [§S-E-AT-HD-HAT] -- Has_Data Attributes [§S-E-AT-HD-HDAT] -- Selected Expressions [§S-E-AT-HD-S] -- List Comprehensions [§S-E-AT-HD-LC] -- Bindings [§S-E-AT-HD-B] -- Quantified Expressions [§S-E-AT-HD-Q] -- Calls [§S-E-AT-HD-CL] -- Conversions [§S-E-AT-HD-CV] -
- -__Dynamic Semantics__ - -The use of the Opaque attribute on an invalid message or the use of the Head attribute on an empty sequence leads to an exception transition. This behavior will change in the future (cf. [#569](https://github.com/Componolit/RecordFlux/issues/569)). - -__Example__ - -```Ada RFLX extended_suffix -Message'Valid -``` - -#### Selected Expressions [§S-E-S] - -The Selected expression is used to get a value of a message field. - -__Syntax__ - -*selected* ::= message_*expression* __.__ field_*name* - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-E-S-ME] -- Literals [§S-E-S-L] -- Variables [§S-E-S-V] -- Message Aggregates [§S-E-S-MA] -- Aggregates [§S-E-S-A] -- Valid Attributes [§S-E-S-VAT] -- Opaque Attributes [§S-E-S-OAT] -- Head Attributes [§S-E-S-HAT] -- Has_Data Attributes [§S-E-S-HDAT] -- Selected Expressions [§S-E-S-S] -- List Comprehensions [§S-E-S-LC] -- Bindings [§S-E-S-B] -- Quantified Expressions [§S-E-S-Q] -- Calls [§S-E-S-CL] -- Conversions [§S-E-S-CV] -
- -__Dynamic Semantics__ - -An access to an invalid message field leads to an exception transition. This behavior will change in the future (cf. [#569](https://github.com/Componolit/RecordFlux/issues/569)). - -__Example__ - -```Ada RFLX extended_suffix -Ethernet_Frame.Payload -``` - -#### List Comprehensions [§S-E-LC] - -A list comprehension provides a way to create a new sequence based on an exisiting sequence. - -__Syntax__ - -*comprehension* ::= __[for__ *name* __in__ iterable_*expression* __=>__ selector_*expression* __when__ condition_*expression* __]__ - -__Static Semantics__ - -
-- Source: Scalar sequence [§S-E-LC-SSS] -- Source: Message sequence [§S-E-LC-SMS] -- Source: Variable [§S-E-LC-V] -- Source: Selected [§S-E-LC-S] -- Target: Scalar sequence [§S-E-LC-TSS] -- Target: Message sequence [§S-E-LC-TMS] -- Condition: Selected [§S-E-LC-CS] -- Source sequence as target [§S-E-LC-SAT] -- Global declarations [§S-E-LC-GD] -- Local declarations [§S-E-LC-LD] -- State transitions [§S-E-LC-T] -- Assignment statements [§S-E-LC-A] -
- -__Dynamic Semantics__ - -An access to an invalid element in iterable_*expression* leads to an exception transition. This behavior will change in the future (cf. [#569](https://github.com/Componolit/RecordFlux/issues/569)). - -__Example__ - -```Ada RFLX extended_primary -[for O in Offer.Options => O.DHCP_Message_Type when O.Code = DHCP::DHCP_Message_Type_Option] -``` - -#### Bindings [§S-E-B] - -A binding can be used to name a subexpression and enables the use of a subexpression multiple times without the need for duplicating the expression or declaring a separate variable. - -__Syntax__ - -*binding* ::= *expression* __where__ *name* __=__ sub_*expression* { __,__ *name* __=__ sub_*expression* } - -__Static Semantics__ - -
-Expressions: - -- Mathematical Expressions [§S-E-B-ME] -- Literals [§S-E-B-L] -- Variables [§S-E-B-V] -- Message Aggregates [§S-E-B-MA] -- Aggregates [§S-E-B-A] -- Valid Attributes [§S-E-B-VAT] -- Opaque Attributes [§S-E-B-OAT] -- Head Attributes [§S-E-B-HAT] -- Has_Data Attributes [§S-E-B-HDAT] -- Selected Expressions [§S-E-B-S] -- List Comprehensions [§S-E-B-LC] -- Bindings [§S-E-B-B] -- Quantified Expressions [§S-E-B-Q] -- Calls [§S-E-B-CL] -- Conversions [§S-E-B-CV] - -For subexpressions the same semantics apply as for assignments. -
- -__Static Semantics__ - -The type of the subexpression is inferred by the subexpression type and the expected type for all references of the name. - -__Example__ - -```Ada RFLX extended_suffix -TLS_Alert::Alert'(Level => Level, Description => Description) - where - Level = TLS_Alert::Fatal, - Description = GreenTLS_Alert_Message.Description -``` - -#### Quantified Expressions [§S-E-Q] - -Quantified expressions enable reasoning about properties of sequences. - -__Syntax__ - -*quantified_expression* ::= __for__ *quantifier* __in__ iterable_*expression* __=>__ predicate_*expression* - -*quantifier* ::= __all__ | __some__ - -__Static Semantics__ - -
-Iterable expressions [§S-E-Q-I]: - -- Mathematical Expressions [§S-E-Q-I-ME] -- Literals [§S-E-Q-I-L] -- Variables [§S-E-Q-I-V] -- Message Aggregates [§S-E-Q-I-MA] -- Aggregates [§S-E-Q-I-A] -- Valid Attributes [§S-E-Q-I-VAT] -- Opaque Attributes [§S-E-Q-I-OAT] -- Head Attributes [§S-E-Q-I-HAT] -- Has_Data Attributes [§S-E-Q-I-HDAT] -- Selected Expressions [§S-E-Q-I-S] -- List Comprehensions [§S-E-Q-I-LC] -- Bindings [§S-E-Q-I-B] -- Quantified Expressions [§S-E-Q-I-Q] -- Calls [§S-E-Q-I-CL] -- Conversions [§S-E-Q-I-CV] - -Predicate expressions [§S-E-Q-P]: - -- Mathematical Expressions [§S-E-Q-P-ME] -- Literals [§S-E-Q-P-L] -- Variables [§S-E-Q-P-V] -- Message Aggregates [§S-E-Q-P-MA] -- Aggregates [§S-E-Q-P-A] -- Valid Attributes [§S-E-Q-P-VAT] -- Opaque Attributes [§S-E-Q-P-OAT] -- Head Attributes [§S-E-Q-P-HAT] -- Has_Data Attributes [§S-E-Q-P-HDAT] -- Selected Expressions [§S-E-Q-P-S] -- List Comprehensions [§S-E-Q-P-LC] -- Bindings [§S-E-Q-P-B] -- Quantified Expressions [§S-E-Q-P-Q] -- Calls [§S-E-Q-P-CL] -- Conversions [§S-E-Q-P-CV] -
- -__Example__ - -```Ada RFLX extended_primary -for all E in Server_Hello_Message.Extensions => E.Tag /= TLS_Handshake::ET_Supported_Versions -``` - -#### Calls [§S-E-CL] - -All functions which are declared in the session parameters can be called. - -__Syntax__ - -*call* ::= *name* [ __(__argument_*expression* { __,__ argument_*expression* } __)__ ] - -__Static Semantics__ - -
-Argument expressions: - -- No argument [§S-E-CL-N] -- Mathematical Expressions [§S-E-CL-ME] -- Literals [§S-E-CL-L] -- Variables [§S-E-CL-V] -- Message Aggregates [§S-E-CL-MA] -- Aggregates [§S-E-CL-A] -- Valid Attributes [§S-E-CL-VAT] -- Opaque Attributes [§S-E-CL-OAT] -- Head Attributes [§S-E-CL-HAT] -- Has_Data Attributes [§S-E-CL-HDAT] -- Selected Expressions [§S-E-CL-S] -- List Comprehensions [§S-E-CL-LC] -- Bindings [§S-E-CL-B] -- Quantified Expressions [§S-E-CL-Q] -- Calls [§S-E-CL-CL] -- Conversions [§S-E-CL-CV] -
- -__Example__ - -```Ada RFLX extended_primary -Decrypt (Key_Update_Message, Sequence_Number, TLS_Record_Message.Encrypted_Record) -``` - -#### Conversions [§S-E-CV] - -An opaque field of a message can be converted to a message. - -__Syntax__ - -*conversion* ::= message_type_*name* __(__message_*expressions* __.__ field_*name*__)__ - -__Static Semantics__ - -
-A conversion is only allowed if a refinement for the message field and the intended target type exists. - -Expressions: - -- Mathematical Expressions [§S-E-CV-ME] -- Literals [§S-E-CV-L] -- Variables [§S-E-CV-V] -- Message Aggregates [§S-E-CV-MA] -- Aggregates [§S-E-CV-A] -- Valid Attributes [§S-E-CV-VAT] -- Opaque Attributes [§S-E-CV-OAT] -- Head Attributes [§S-E-CV-HAT] -- Has_Data Attributes [§S-E-CV-HDAT] -- Selected Expressions [§S-E-CV-S] -- List Comprehensions [§S-E-CV-LC] -- Bindings [§S-E-CV-B] -- Quantified Expressions [§S-E-CV-Q] -- Calls [§S-E-CV-CL] -- Conversions [§S-E-CV-CV] -
- -__Dynamic Semantics__ - -An invalid condition of a refinement leads to an exception transition. This behavior will change in the future (cf. [#569](https://github.com/Componolit/RecordFlux/issues/569)). - -__Example__ - -```Ada RFLX extended_primary -Key_Update_Message (Handshake_Control_Message.Data) -``` - -## Package - -A package is used to structure a specification. - -#### Syntax - -*package* ::= __package__ *name* __is__ *body* __end__ *name* __;__ - -*body* := { *modular_type* | *range_type* | *enumeration_type* | *message_type* | *type_refinement* | *session* } - -#### Static Semantics - -A package is a collection of types and sessions. By convention one protocol is specified in one package. - -#### Example - -```Ada RFLX -package Ethernet is - - type Address is mod 2**48; - type Type_Length is range 46 .. 2**16 - 1 with Size => 16; - type TPID is range 16#8100# .. 16#8100# with Size => 16; - type TCI is mod 2**16; - type Ether_Type is - (ET_IPv4 => 16#0800#, - ET_ARP => 16#0806#, - ET_VLAN_Tag => 16#8100#, - ET_IPv6 => 16#86DD#, - ET_VLAN_Tag_Double => 16#9100#) - with Size => 16, Always_Valid; - - type Frame is - message - Destination : Address; - Source : Address; - Type_Length_TPID : Type_Length - then TPID - with First => Type_Length_TPID'First - if Type_Length_TPID = 16#8100# - then Payload - with Size => Type_Length_TPID * 8 - if Type_Length_TPID <= 1500 - then Ether_Type - with First => Type_Length_TPID'First - if Type_Length_TPID >= 1536 and Type_Length_TPID /= 16#8100#; - TPID : TPID; - TCI : TCI; - Ether_Type : Ether_Type - then Payload - with Size => Message'Last - Ether_Type'Last; - Payload : Opaque - then null - if Payload'Size / 8 >= 46 and Payload'Size / 8 <= 1500; - end message; - -end Ethernet; -``` - -## Context Clause - -The context clause is used to specify the relation to other packages and consists of a list of with clauses. - -#### Syntax - -*context* ::= { __with__ *package_name* __;__ } - -*package_name* ::= *name* - -#### Static Semantics - -For each package referenced in a file, a corresponding with clause has to be added to the beginning of the file. - -#### Example - -```Ada RFLX context_clause -with Ethernet; -with IPv4; -``` - -## File - -A RecordFlux specification file is recognized by the file extension `.rflx`. Each specification file contains exactly one package. The file name must match the package name in lower case characters. - -#### Syntax - -*file* ::= *context* *package* - -#### Example - -File: `in_ethernet.rflx` - -```Ada RFLX specification -with Ethernet; -with IPv4; - -package In_Ethernet is - - for Ethernet::Frame use (Payload => IPv4::Packet) - if Ether_Type = Ethernet::ET_IPv4; - -end In_Ethernet; -``` diff --git a/setup.py b/setup.py index c85b96c3e7..f363e318d2 100644 --- a/setup.py +++ b/setup.py @@ -7,7 +7,7 @@ assert match version = match.group(1) -with open("README.md") as f: +with open("README.adoc") as f: readme = f.read() setup( diff --git a/tests/unit/cli_test.py b/tests/unit/cli_test.py index d8cafb9ebf..b7e3e7bc44 100644 --- a/tests/unit/cli_test.py +++ b/tests/unit/cli_test.py @@ -48,17 +48,17 @@ def test_main_check_quiet() -> None: def test_main_check_parser_error(monkeypatch: Any) -> None: monkeypatch.setattr(cli, "check", lambda x: raise_parser_error()) - assert ":8:22: parser: error: TEST" in str(cli.main(["rflx", "check", "README.md"])) + assert ":8:22: parser: error: TEST" in str(cli.main(["rflx", "check", "README.adoc"])) def test_main_check_model_error_parse(monkeypatch: Any) -> None: monkeypatch.setattr(cli, "check", lambda x: raise_model_error()) - assert ":8:22: model: error: TEST" in str(cli.main(["rflx", "check", "README.md"])) + assert ":8:22: model: error: TEST" in str(cli.main(["rflx", "check", "README.adoc"])) def test_main_check_model_error_create_model(monkeypatch: Any) -> None: monkeypatch.setattr(rflx.specification.Parser, "create_model", lambda x: raise_model_error()) - assert ":8:22: model: error: TEST" in str(cli.main(["rflx", "check", "README.md"])) + assert ":8:22: model: error: TEST" in str(cli.main(["rflx", "check", "README.adoc"])) def test_main_check_non_existent_file() -> None: diff --git a/tools/check_doc.py b/tools/check_doc.py index 90778bbeef..6ea8d9d6bb 100755 --- a/tools/check_doc.py +++ b/tools/check_doc.py @@ -26,34 +26,44 @@ class CodeBlockType(enum.Enum): PYTHON = enum.auto() +class State(enum.Enum): + OUTSIDE = enum.auto() + INSIDE = enum.auto() + HEADER = enum.auto() + + def check_code_blocks() -> bool: valid = True code_blocks = [] - inside = False + state = State.OUTSIDE - for p in [pathlib.Path("README.md")] + list(pathlib.Path("doc").rglob("*.md")): + for p in [pathlib.Path("README.adoc")] + list(pathlib.Path("doc").rglob("*.adoc")): with open(p) as f: for l in f: - if not inside and l.startswith("```"): - inside = True + if state == State.OUTSIDE and l.startswith("[source"): + state = State.HEADER block = "" - if l.startswith("```Ada RFLX"): + if l.startswith("[source,ada,rflx"): block_type = CodeBlockType.RFLX - subtype = l[12:-1] - elif l == "```Ada\n": + subtype = l[17:-2] + elif l == "[source,ada]\n": block_type = CodeBlockType.ADA - elif l == "```Python\n": + elif l == "[source,python]\n": block_type = CodeBlockType.PYTHON else: block_type = CodeBlockType.UNKNOWN continue - if inside and l.startswith("```"): - inside = False + if state == State.HEADER and l == "----\n": + state = State.INSIDE + continue + + if state == State.INSIDE and l == "----\n": + state = State.OUTSIDE code_blocks.append((block_type, subtype, block)) continue - if inside: + if state == State.INSIDE: block += l ("build" / SPEC_DIR.parent).mkdir(parents=True, exist_ok=True)