Users guide

[senier]

Motivation

• Simplify learning how to use language and tools

Description

Explain all details necessary for using RecordFlux (to be extended into a document outline):

• Installation
• Specification language
  • #342
  • Sessions
    • IO states
    • Exception transitions
• CLI
  • --help for rflx and all sub-commands
• Verifier
  • Properties proven
  • Style checks
  • Caching of successful verification results
  • rflx check
• Generator
  • Integration files (*.rfi)
  • Use in SPARK programs
    • Implementing channel interfaces and external functions
  • Ada runtime requirements
  • Memory management
  • rflx generate
  • Semantics of API (e.g, differences between structural valid and valid, cf. https://github.com/Componolit/RecordFlux/issues/972#issuecomment-1088556809)
• Simulator
  • Use in Python (PyRFLX)
• Validator
  • Parameter files (*.yaml)
  • Workflow when validating message specifications
  • Coverage analysis
  • rflx validate
• Modeler (IDE)
• Visualizer
  • Generating graphical representation of models
  • rflx graph
• IANA tool
• Integration into build system / CI
  • Make example
• Tutorial / complex example
  • Specifying protocol and verifying (TBD)
    • Consider using sequences and refinements
    • Example for parameterized messages and #609
  • Rapid prototyping using PyRFLX
  • Generation of SPARK code
  • Implement generator/parser
  • Proof program
  • Run/test program
• Errors
  • Error references: Add unique identifiers to error messages and explain each error
  • Bug box
  • How to report errors
• Language reference

[treiher]

Here are some notes from Feb 14 about the specification language for sessions. I think it makes sense to collect that information here instead of leaving it on some branch.

---

Specification Language

Sessions

Memory Model

• Assignment of Result := Message leads to a copy of Message
• Static reservation of memory for declared message variables
  • Static size determined by default value
  • Optimizations:
    • Determine maximum length of message type from specification, use default value for unbounded messages
    • Introduce scoped variables which are reused (static allocation of pointers to scope)
• Potential issues:
  • References may be desirable if large data would be copied in assignment

Channels

Properties

• Reliable
• Order-preserving
• Interface:
  • Synchronous/blocking
  • Variable-sized packets

Interface

~Message := Read (Channel)~ Channel'Read (Message)

• Copy next message from Channel into target buffer Message

~Success := Write (Channel, Message)~ Channel'Write (Message)

• Copy Message into Channel
• ~Return True if successful~

~Result_Message := Call (Channel, Message)~

• ~Call Write (Channel, Message) and Result_Message := Read (Channel) consecutively~
• ~Result_Message'Valid yields True if successful and Result_Message is valid according to its type~

Success := Data_Available (Channel)

• Return True if message is available in Channel

Possible extension:

• Function or attribute on channel for determining if sending message was successful

[senier]

Here are some notes from Feb 14 about the specification language for sessions. I think it makes sense to collect that information here instead of leaving it on some branch.

It fits even better into #291.

[treiher]

I'm not sure, the focus of #291 is the syntax while these notes are more about the semantics. As I see no big benefit in moving the notes, I would just keep them here.