Expression#

An expression is a typed formal statement that evaluates to a value. Expressions are present in two cases:

In formal Requirement to express a property that must hold
In Attribute definition to express the domain of the attribute

An expression composes several attributes in order to:

Define a formal property that must hold considering the domain of the involved attributes
Constrain an attribute to narrow its definition domain

Attention

An expression is not an algorithm. There are no instructions or sequences of actions — only properties that must hold.

Formalism#

req uses several formalisms in conjunction to produce expressions:

Allowed formalisms#
Name	Examples
Propositional logic	`and`, `or`
LTL (discrete-time)	`always`, `eventually`
FOL	`forall`, `exists`
Set theory	`includes`, `in`
Common algebra	`+`, `-`

Note

The current set of formalisms is a deliberate subset of what a specification may require. req will progressively be extended with additional constructs: the guiding criterion is that any new construct must be expressible in standard formal notation and relevant for systems engineers.

In req, every attribute is treated as a signal that may change over time — similar to a measured variable in a control system or a recorded parameter in a flight data recorder. Formally, the attributes used in expressions are considered time-dependent functions.

Suppose an attribute is defined by a requirement as:

\[x = f(y, z)\]

where \(f\) denotes an expression. It is assumed that \(x\), \(y\), and \(z\) are functions of time, i.e.:

\[\forall t\quad x(t) = f(y(t), z(t))\]

As a corollary, \(x\) is constant if and only if \(y\) and \(z\) are constants (such as literals).

Note

Unless explicitly stated by temporal operators, attribute constraints hold for all \(t\) — that is, across the entire system lifecycle and all operating conditions. This scope can be narrowed by introducing attributes that represent specific operating conditions or lifecycle phases.

Type system#

The type of an expression defines which operators can be applied to it. An attribute has a type that is inferred from its domain definition.

Operators in req are strictly typed: applying an operator to an expression of an incompatible type is not allowed.

If a type cannot be inferred, the expression has the type undefined, which is not a true type but denotes the absence of typing information.

Attention

While there is currently no mechanism to define a custom type, this is subject to change.

Number#

The type Number covers all numerical values, including integers and real numbers. No distinction is made between them in the type system.

Boolean#

The type Boolean is applied to any boolean expression.

Set#

The type Set(T) is applied to any expression that evaluates to a set. Sets are homogeneous in the sense that they can only contain elements of the same type.

Literals#

A literal is a value written directly in the expression source.

Numbers#

Numbers are written in decimal format and may use exponential notation.

Example of numbers#

 2
 3.14
 10e7

infinity represents an infinite value. Values are of type Number.

Note

No distinction is made between integers and real numbers at the type level. Fractional expressions such as 1/3 are evaluated as arithmetic operations, not written as decimal literals.

Boolean#

The Boolean literals true and false represent the two truth values.

Booleans#

 true
 false

Values are of type Boolean.

Set#

The set literal allows creating an ad-hoc set with a finite number of elements:

Syntax of set#

{ <EXPRESSION (, EXPRESSION)+|EXPRESSION?> }

Example of set literal#

{1, 2, 3}

Values are of type Set. Expressions must have the same type.

Built-in set#

A built-in set is a keyword that denotes a well-known set:

Built-in sets#

real
boolean
integer

Note

Built-in sets are most commonly used as the domain of an attribute.

Values are of type Set. Element type varies according to the built-in set.

Operators#

An operator is an expression that contains one or more operands (attributes or literals). Each operator is paired with a formal equivalent that translates the req expression into standard mathematical notation.

Note

Throughout this section, lowercase x and y denote scalar values, and uppercase X and Y denote sets (domains).

Grouping#

Any sub-expression may be enclosed in parentheses to make evaluation order explicit:

Syntax#

 ( EXPRESSION )

Parentheses always override the default precedence and associativity rules described in the Precedence section below.

Arithmetic#

Arithmetic operators act on Number and evaluate to Number.

Arithmetic operators#
Syntax	Description	Formal equivalence
`x + y`	Addition	\(x + y\)
`x - y`	Subtraction	\(x - y\)
`x * y`	Multiplication	\(x \cdot y\)
`x / y`	Division	\(x / y\)
`x % y`	Remainder	\(x \bmod y\)
`x ^ y`	Exponentiation	\(x^{y}\)
`-x`	Unary negation	\(-x\)
`+x`	Unary identity	\(+x\)
`x!`	Factorial	\(x!\)

Equality#

Equality operators act on every type and evaluate to Boolean. In req, equality is always by value, the concept of reference does not exists.

Comparison operators#
Syntax	Description	Formal equivalence
`x = y`	True if x and y are equal	\(x = y\)
`x /= y`	True if x and y are not equal	\(x \neq y\)

Attention

In req, = is always an equality test, never an assignment. The expression altitude = 120 in a requirement body means “altitude shall be equal to 120”.

Comparison#

Comparison operators act on Number and evaluate to Boolean.

Comparison operators#
Syntax	Description	Formal equivalence
`x < y`	True if x is strictly less than y	\(x < y\)
`x > y`	True if x is strictly greater than y	\(x > y\)
`x <= y`	True if x is less than or equal to y	\(x \leq y\)
`x >= y`	True if x is greater than or equal to y	\(x \geq y\)

Propositional logic#

Propositional logic operators act on Boolean and evaluate to Boolean.

Propositional logic operators#
Syntax	Description	Formal equivalence
`x and y`	True if both x and y are true	\(x \wedge y\)
`x or y`	True if at least one of x or y is true	\(x \vee y\)
`x xor y`	True if exactly one of x or y is true	\(x \oplus y\)
`x implies y`	True if x is false or x and y are true	\(x \Rightarrow y\)
`x iff y`	True if x and y have the same truth value	\(x \Leftrightarrow y\)
`not x`	True if x is false	\(\neg x\)

Set#

The following operators act on Set and evaluate to Set.

Set algebra operators#
Syntax	Description	Formal equivalence
`X union Y`	Elements belonging to X or Y	\(X \cup Y\)
`X intersection Y`	Elements belonging to both X and Y	\(X \cap Y\)
`X difference Y`	Symmetric difference of X and Y	\(X \Delta Y = (X \cup Y) \setminus (X \cap Y)\)
`X complement Y`	Elements of X that are not in Y	\(X \setminus Y\)

The following operators act on Set and evaluate to Boolean.

Set predicate operators#
Syntax	Description	Formal equivalence
`x in X`	True if x is an element of X	\(x \in X\)
`X includes Y`	True if Y is a subset of X	\(Y \subseteq X\)

Temporal logic#

Temporal logic operators act on Boolean and evaluate to Boolean. They express properties over a discrete sequence of time steps. See LTL for the underlying formalism.

Temporal logic operators#
Syntax	Description	Formal equivalence
`always x`	True if x holds at every future time step	\(\square x\)
`eventually x`	True if x holds at some future time step	\(\lozenge x\)
`previously x`	True if x held at the immediately preceding time step	\(\ominus x\)
`rising x`	True at the first time step where x becomes true	\(\neg x_{t-1} \wedge x_{t}\)
`falling x`	True at the first time step where x becomes false	\(x_{t-1} \wedge \neg x_{t}\)
`x since y`	True if x has been true at every step since the last step where y was true	\(x \,\mathcal{S}\, y\)

Note

The notion of time step does not refer to a particular time division or sampling rate. Time steps can be thought of as an arbitrary division that splits continuous time into event points at which state changes occur (i.e., the values of the attributes change).

Aggregator#

An aggregator takes a list of expressions as arguments and evaluates to a single value.

Syntax#

<all|any> EXPRESSION (, EXPRESSION)* end

Aggregators#
Syntax	Description	Formal equivalence
`all x1, x2, ... end`	True if all arguments are true	\(\bigwedge x_i\)
`any x1, x2, ... end`	True if at least one argument is true	\(\bigvee x_i\)

Example of aggregators#

 requirement R is
  all
   speed < max_speed,
   altitude < max_altitude,
   fuel_level > reserve
  end
 requirement

Note

Boolean aggregators are the list counterparts of and and or: all e1, e2 end is equivalent to e1 and e2, and any e1, e2 end is equivalent to e1 or e2.

Function call#

A function call applies an expression to a list of arguments:

Syntax#

 EXPRESSION ( EXPRESSION (, EXPRESSION)* )

Attention

Function calls are recognised by the parser but are not yet type-checked or evaluated by the compiler. This construct is reserved for future use.

Conditional#

A conditional is a notation for expressing a requirement that depends on one or more conditions. It is a direct equivalent of a propositional pattern and does not add expressive power — only readability.

Branch#

The branch conditional is an expression whose content depends on a condition:

Syntax#

 if EXPRESSION then EXPRESSION
 (else EXPRESSION)?
 end

Example of if#

 requirement R is
  if doors_open then speed = 0
  else speed < 25
  end
 requirement

Let \(c\) denote the condition, \(x\) the consequence (the expression when the condition is true) and \(y\) the fallback. The if-else expression is strictly equivalent to:

\[(c \Rightarrow x) \wedge (\neg c \Rightarrow y)\]

If the else branch is not defined, \(y\) is taken equal to true by convention, that is, the expression becomes:

\[c \Rightarrow x\]

All expressions must be of type Boolean.

When#

The when conditional is an expression governed by a set of unordered conditions:

Syntax#

 when
   EXPRESSION then EXPRESSION
   (, EXPRESSION then EXPRESSION)*
   (otherwise EXPRESSION)?
 end

Example of when#

 requirement R is
  when
   doors_open then speed = 0,
   weather_is_bad then speed < 10,
   otherwise speed < 25
  end
 requirement

Let \(c_i\) denote the conditions, \(x_i\) the consequences for each condition and \(y\) the fallback. The when expression is strictly equivalent to:

\[\left(\bigwedge_i c_i \Rightarrow x_i\right) \wedge \left(\left(\bigwedge_i \neg c_i\right) \Rightarrow y\right)\]

If the otherwise branch is not defined, \(y\) is taken equal to true by convention, which simplifies the expression:

\[\bigwedge_i c_i \Rightarrow x_i\]

All expressions must be of type Boolean.

Note

This construct is particularly useful when multiple conditions govern a requirement simultaneously — for instance, when specifying an event-action mechanism such as a state machine.

Quantifiers#

A quantifier is an expression that evaluates over the elements of a set. By convention, in this section, \(x\) denotes the identifier, \(X\) the domain (expression after the in), \(P(x)\) the filter (expression after the such that).

Forall#

The forall quantifier is strictly equivalent to the universal quantifier of first-order logic \(\forall\).

Syntax#

 forall IDENTIFIER in EXPRESSION (such that EXPRESSION)?
   EXPRESSION
 end

Example of forall#

 requirement R is
   forall t in train_units such that t::speed = 0
     t::alarm_triggered
   end
 requirement

The expression evaluates to Boolean. Denote the body expression \(Q(x)\); the forall block is strictly equivalent to:

\[\forall x \in X,\ P(x) \Rightarrow Q(x)\]

When the such that clause is omitted, \(P(x)\) is taken equal to \(\text{true}\), which simplifies to:

\[\forall x \in X,\ Q(x)\]

Note

If the domain is empty, forall evaluates to true (vacuous truth).

Exists#

The exists quantifier is strictly equivalent to the existential quantifier of first-order logic \(\exists\).

Syntax#

 exists IDENTIFIER in EXPRESSION
   such that EXPRESSION
 end

Example of exists#

 requirement R is
   exists t in train_units such that t::ready_for_departure
   end
 requirement

The expression evaluates to Boolean. Unlike forall, exists has no body expression: the such that clause is the predicate. The exists block is strictly equivalent to:

\[\exists x \in X,\ P(x)\]

Note

If the domain is empty, exists evaluates to false.

Select#

The select quantifier has no first-order logic equivalent. It expresses the choice of an element within a set.

Syntax#

 select IDENTIFIER in EXPRESSION (such that EXPRESSION)?
   (<maximizes|minimizes> EXPRESSION)?
 end

Example of select#

 requirement R is
   closest_plane = select p in managed_planes
     minimizes p::distance_to_runway_threshold
   end
 requirement

The expression evaluates to an element drawn from the input domain. The optional maximizes or minimizes part is called the optimizer.

Attention

If the input domain is empty, the evaluation of the select is undefined.

Denote \(a\) the value the select block evaluates to and \(f(x)\) the optimizer expression. Suppose the optimizer is a maximization; \(a\) has the following property:

\[a \in X \wedge a = \underset{x \in X,\, P(x)}{\mathrm{argmax}}\ f(x)\]

The minimization case is symmetric:

\[a \in X \wedge a = \underset{x \in X,\, P(x)}{\mathrm{argmin}}\ f(x)\]

When no optimizer is specified but a such that clause is present, the select guarantees:

\[a \in X \wedge P(a)\]

When neither optimizer nor filter is specified:

\[a \in X\]

Note

The choice is non-deterministic. Using the non-optimized form is useful to constrain intermediate attributes or quantities that serve as inputs to other requirements.

Precedence#

The table below lists all operators from lowest to highest precedence. Operators on the same row have equal precedence. When in doubt, use parentheses to make evaluation order explicit.

Operator precedence (lowest to highest)#
Operators	Associativity
`iff` `implies`	Left
`or` `xor`	Left
`and`	Left
`not` (prefix)	—
`always` `eventually` `previously` `rising` `falling` (prefix)	—
`since`	Left
`union` `difference`	Left
`intersection`	Left
`complement`	Left
`in` `includes`	Left
`=` `/=`	Left
`<` `>` `<=` `>=`	Left
`+` `-`	Left
`*` `/` `%`	Left
`^`	Right
Unary `-` `+` `not`	—
`x!`	—
`f(...)`	Left

Expression#

Formalism#

Type system#

Number#

Boolean#

Set#

Literals#

Numbers#

Boolean#

Set#

Built-in set#

Operators#

Grouping#

Arithmetic#

Equality#

Comparison#

Propositional logic#

Set#

Temporal logic#

Aggregator#

Function call#

Conditional#

Branch#

When#

Quantifiers#

Forall#

Exists#

Select#

Precedence#

This Page