Getting started#

This tutorial walks you through the initial setup of the req language tools and the writing of your first specification.

Prerequisites#

The language and tools are straightforward to use, but it is preferable that you are familiar with:

  • The use of the terminal, PowerShell for Windows and sh for macOS and Linux

  • The use of an IDE, VSCode preferentially

It is recommended that you have VSCode installed on your machine. You can download it here.

Setup#

This section will guide you through the installation of the required tools to start specifying with the req language.

Note

To perform an advanced setup refer to the tooling section of this documentation.

reqtool#

reqtool is the only binary you will need to install. It is a general utility program that we will use to check the validity of a specification.

To install reqtool, open a terminal and copy the command below:

curl -fsSL https://raw.githubusercontent.com/req-lang/reqtool/main/install.sh | sh

irm https://raw.githubusercontent.com/req-lang/reqtool/main/install.ps1 | iex

Authentication might be required to finalize the setup. Once it is done you should be able to run the following command:

reqtool help

A help message should be displayed indicating the available commands and the usage of the program.

req-vscode#

This is the VSCode extension that provides syntax coloring and other features for editing specifications in the IDE. It is recommended that you use it for this tutorial.

  1. Go to the extension releases req-lang/req-vscode

  2. Download the req-vscode.vsix file

  3. Follow the official instructions to install a .vsix extension

Open a new text file and save it with the .req extension. Copy the following code into the newly created file:

Template code#
 package System
   part Model
   part

   package Requirements
   package
 package

If everything works, you should see the keywords and labels highlighted.

Hint

This code represents the standard structure of most specifications in req. You will likely use it as a starting point very often.

Your first specification#

In this section we will set up a basic workflow so you understand how to work with req.

Use the checker#

Create a new file named intro.req. Copy-paste the above req code into this file. Then open a terminal at the directory where the file is located and execute the following command:

reqtool check intro.req

You should see a single line output saying something like:

All done in 64.20us

The check command performed a verification of the file intro.req to diagnose any issues.

Note

The VSCode extension performs checks automatically on save. The command line interface is used here for clarity.

Adding a requirement#

Within the Requirements package, add the following:

requirement Maximum_temperature is
  @@
    The system temperature shall be less than 30C
  @@
requirement

This passes the check and looks like most requirements you have written in Excel or any ALM tool.

While this is a perfectly valid way to use req, in the next section you will understand what the preferred approach is and why it matters.

Adding an attribute#

Consider the following question: what if several requirements deal with temperature and you want to identify exactly which ones?

This question comes up naturally when searching for contradictions or analyzing the impact of a change. The notion of Attribute and Part was introduced precisely for this. Let’s add an attribute under the Model part:

let temperature in real [C]

And now let’s use this attribute:

requirement Maximum_temperature is
  @@
    The {System::Model::temperature} shall be less than 30C
  @@
requirement

Maximum_temperature is now explicitly linked to temperature. There is no need to search the specification manually to find requirements related to the concept of system temperature.

Hint

When extracting a part or an attribute reference, always prefer the narrowest scope. In the above requirement, we could have written The {System} temperature shall be less than 30C, but that would lose precision: the requirement constrains a specific attribute, not the system as a whole.

Your first diagnostic#

For the sake of demonstration, delete the temperature attribute we just created and run reqtool check intro.req.

The command outputs an error message that looks like this:

Reference not found: System::Model::temperature
 8:7

This is a diagnostic established during the check, indicating that the requirement (line 8, column 7) references something that does not exist.

The check command acts like a compiler for your specifications. A wide variety of diagnostics can be reported; a description of each is available in the Language Reference.

Switching to formal#

The requirement we wrote is valid and makes the specification easy to browse. Two things can still be improved:

  1. Writing the requirement in plain English adds boilerplate that carries no mathematical meaning.

  2. We lose the precise semantics of what we expect from the attribute.

Formal notation addresses both: expressions are concise, and each formal requirement in req is implicitly a shall statement.

By preserving the mathematical meaning of the requirement, the compiler can also detect formal contradictions and catch an entirely different class of errors.

Let’s rewrite our requirement in formal notation:

requirement Maximum_temperature is
    System::Model::temperature < 30
requirement

If we had mistakenly written:

requirement Maximum_temperature is
    System::Model::temperature < false
requirement

The check command would report:

Expected Number got Boolean
    8:35

This is first-class type checking applied to your specification.

Make a refinement#

So far we have written a single requirement. When working with multiple requirements, it is common to make the relationships between them explicit. Here is how to do that in req.

Let’s add a higher-level requirement than the one we have been working with:

requirement Bound_temperature is
  @@
    The {System::Model::temperature} shall be bound.
  @@
requirement

Now let’s express the traceability link using refines. Modify the Maximum_temperature requirement:

requirement Maximum_temperature
refines System::Requirements::Bound_temperature
is
    System::Model::temperature < 30
requirement

Complete example#

Once done, you should end up with the following content in intro.req:

package System
  part Model
    let temperature in real [C]
  part

  package Requirements
    requirement Bound_temperature is
      @@
        The {System::Model::temperature} shall be bound.
      @@
    requirement

    requirement Maximum_temperature
    refines System::Requirements::Bound_temperature
    is
      System::Model::temperature < 30
    requirement
  package
package

This specification should pass the check with no diagnostics.

Wrapping up#

In this tutorial you learned how to set up the toolchain for the req language and make use of the compiler diagnostics. You were introduced to the most common workflow:

  1. Write in plain English

  2. Extract attributes and parts from the requirements

  3. Formalize and trace where relevant

  4. Check and fix via reqtool check

You have built a specification that is:

  • Formal, with mathematical and logical properties that are enforced by the compiler

  • Easily browsable, traceable, and analyzable