L.O.B.S.T.E.R.

text: All input files are encoded in UTF-8. Passing a file with a
different encoding to TRLC results in
undefined behaviour.

text: It is recommended to try to detect this in an implementation
and raise a fatal error; but in the interest
of compatibility and sanity an
implementation shall not provide a way to
switch the encoding (at the command-line or
otherwise).

text: Whitespace is ignored.

text: Comments are C-Style `/* .. */` and C++ style `//`, and are
ignored. The matching for C-style comments
is non-greedy.

text: Identifiers start with a letter and are followed by letters,
numbers, or underscores.

text: A keyword is an identifier that is one of the following
reserved words:

bullets: ['abs', 'abstract', 'and', 'checks', 'else', 'elsif', 'enum', 'error', 'exists', 'extends', 'false', 'fatal', 'final', 'forall', 'freeze', 'if', 'implies', 'import', 'in', 'not', 'null', 'optional', 'or', 'package', 'section', 'separator', 'then', 'true', 'tuple', 'type', 'warning', 'xor']

text: Single character delimiters:

bullets: ['Brackets: `(` `)` `[` `]` `{` `}`', 'Punctuation: `,` `.` `=`', 'Operators: `*` `/` `%` `+` `-`', 'Boolean operators: `<` `>`', 'Symbols: `@` `:` `;`']

text: Double character delimiters:

bullets: ['Operators: `**`', 'Boolean operators: `==` `<=` `>=` `!=`', 'Punctuation: `=>` `..`']

text: Preference is (obviously) given to longer delimiters if
there is ambiguity; i.e. `==` takes
precedence over two `=` tokens.

text: Integers are base 2 (prefixed by `0b`), 10, or 16 (prefixed
by `0x`), and leading zeros are effectively
ignored. It is possible to separate digit
groups with an underscore for
readability. It shall be a lexing error to
use digits that do not fit into the base.

text: Decimals are base 10, and leading and trailing zeros are
effectively ignored.

text: There are three versions of a string, double quoted,
triple single quoted, and triple double quoted:

text: The value of a double quoted string is precisely the
characters between the two double quotes,
with all instances of the `\"` escape
sequence being replaced with `"`.

text: The value of a triple quoted string is the whitespace
trimmed string of characters between the triple quotes
(including the line breaks), The common whitespace at
the beginning of each line (ignoring blank lines) starting
at the second is removed. The trailing whitespace on
every line is removed. There is no escaping in a triple
quoted string.

text: There are two types of files:

bullets: ['`.rsl` They contains the user-defined type definitions and\noptionally user-defined warnings or checks', '`.trlc` They contain instances of the types (this is where\nyour requirements go)']

text: First, all `.rsl` files are parsed. Then, if no errors
are raised, all `.trlc` files are parsed.

text: After all files are parsed, references are resolved and
user-defined checks are applied.

text: All files start with a package indication and an optional import list.

bnf: file_preamble ::= package_indication
{ import_clause }

package_indication ::= 'package' IDENTIFIER_name

import_clause ::= 'import' IDENTIFIER_name

text: The package indication defines the "current package".

text: A package may be imported, in which case its name may be
used as the prefix of a `qualified_name`.

text: A package may not import itself.

text: A `.rsl` file starts with a package declaration and is
followed by type declarations.

bnf: rsl_file ::= file_preamble
{ type_declaration | check_block }

text: A package indication in an `.rsl` file declares a
package. Any given package name may only be
declared once globally.

text: In a `.rsl` file, a package may not import a package that
imports itself, directly or indirectly.

text: An implementation shall support the following builtin types,
that shall be made available for all packages:

bullets: ['Boolean', 'Integer', 'Decimal', 'String', 'Markup_String']

text: A `Boolean` has two values, `false` and `true`.

text: An `Integer` is a signed integer, with an implementation
defined range. This range shall be at least
-1000 to 1000, and this can be infinite.

text: A `Decimal` is a signed rational with a power-of-ten
denominator, with an implementation defined
range. This range for the numerator shall be
at least -1000 to 1000, and denominator is
always a natural number with a range of at
least 1 to 1000. Any of these ranges can be
infinite (but the denominator is always
non-negative).

text: A `String` is a sequence of implementation defined
characters. *(The decision to support Unicode
or not is left unspecified.)* The maximum
length of a String, if any, is implementation
defined, but shall be at least 1000.

text: A `Markup_String` is identical to a `String`, except for a
few additional constraints on the string
contents. Any value of type `Markup_String` is
a valid instance of `String`, but not the
other way around.

text: A package also includes a number of builtin functions that
are made available:

bullets: ['len', 'startswith', 'endswith', 'matches', 'oneof']

text: A package also makes available a number of numeric type
conversion functions:

bullets: ['Integer', 'Decimal']

bnf: described_name ::= IDENTIFIER_name [ STRING_description ]

text: A described name names an entity. The optional string
description has no static or dynamic
semantics.

text: Two described names are considered equal if their names are
equal.

bnf: qualified_name ::= [ IDENTIFIER_package_name '.' ] IDENTIFIER_name

text: The package name of a qualified name must be the current
package or an imported package.

text: The name must be a valid symbol in the current scope (if no
package is provided) or a valid symbol of the
indicated package.

bnf: type_declaration ::= enumeration_declaration
| tuple_declaration
| record_declaration

text: It is an error to create a type with a name that is already
visible. (Note: this especially includes
shadowing one of the builtin types, but also
means you cannot shadow packages.)

bnf: enumeration_declaration ::= 'enum' described_name
'{' { enumeration_literal_specification } '}'

enumeration_literal_specification ::= described_name

text: Each described name declares an enumeration literal
specification, which shall have a unique name
in that enumeration.

text: It is an error to specify an (empty) enumeration without any
literals.

bnf: tuple_declaration ::= 'tuple' described_name
'{' field_declaration
{ [ separator_declaration ]
field_declaration }
'}'

field_declaration ::=
described_name [ 'optional' ] qualified_name_FIELD_TYPE

separator_declaration ::=
'separator' separator_symbol

separator_symbol ::= IDENTIFIER
| '@'
| ':'
| ';'

text: A field type names any valid visible and complete
type. *(Specifically you may not have a recursive
tuple reference.)*

text: A tuple type shall declare separators between all
fields, or none of them.

text: A tuple type with separators may not contain fields
that have tuple types with separators. *(This is to
avoid parsing ambiguities for values such as `1; 2;
3`.)*

text: Only tuples with separators may use optional fields. Tuples
without separators cannot have optional fields.

text: After an optional field has been declared, all fields
following it must also be optional.

text: It is an error to declare two fields with the same
name in the same tuple. *(Note that it is possible,
but a bad idea, to have a separator with the same
identifier as a field.)*

text: There is a potential source of ambiguity between
tuples with two or more integers separated by a `x`
or `b`. This is resolved by giving precedence to the
lexer. For example the string `0x123` should yield
the hex integer 291; but the string `0 x123` or `0 x
123` will generate the tuple. It is recommended to
warn when building tuples where a `b` or `x`
separator follows an integer.

bnf: check_block ::= 'checks' IDENTIFIER_record_or_tuple_name
'{' { check_declaration } '}'

check_declaration ::= expression ','
[ severity ] STRING_message
[ ',' STRING_details ]
[ ',' IDENTIFIER_component_name ]

severity ::= 'warning'
| 'error'
| 'fatal'

text: It is an error to refer to a type that does not exist in the
current package, or is not a record or tuple type.

text: In a check declaration or expression, it is an error to
refer to a component name (or field name) that does not belong
to the record (or tuple respectively) indicated.

text: It is an error to include a newline in the message.

text: Each check inside a check block is evaluated in the specified
order.

text: For record extensions, all checks for the base record must
be evaluated before any check of the record
extension is evaluated.

text: If the evaluated expression is true, no action is taken. If
it is false, then a diagnostic is emitted with
the specified message and details. It is
implementation defined if and how the details
are shown, for example in a "brief" mode they
could be omitted.

text: The severity, if provided, controls how future errors are
treated, and how the TRLC implementation
terminates.

bullets: ['A warning has no effect other than emitting the message.', 'An error (the default, in case severity is not specified)\ncauses an implementation to eventually\nreturn a non-zero error code, but further\nchecks will be evaluated (potentially\ncreating more messages).', 'A fatal message is like an error, except that no further\nchecks from this check block shall be\nevaluated for this object.']

bnf: expression ::= relation { 'and' relation }
| relation { 'or' relation }
| relation [ 'xor' relation ]
| relation [ 'implies' relation ]

bnf: relation ::= simple_expression [ comparison_operator simple_expression ]
| simple_expression [ 'not' ] 'in' membership_choice
| simple_expression [ 'not' ] 'in' simple_expression

membership_choice ::= simple_expression '..' simple_expression

bnf: simple_expression ::= [ adding_operator ]
term { adding_operator term }

bnf: term ::= factor { multiplying_operator factor }

bnf: factor ::= primary [ '**' primary ]
| 'not' primary
| 'abs' primary

bnf: primary ::= INTEGER
| DECIMAL
| STRING
| 'true'
| 'false'
| 'null'
| name
| '(' expression ')'
| '(' quantified_expression ')'
| '(' conditional_expression ')'

text: The parsing of unary minus can be confusing: `-a % b` is
actually `- (a % b)`. The semantics of `%` are
carefully specified so that this does not
matter. It does also mean that `-a / -b` is
not legal and needs to be written as either
`-a / (-b)` or even better `(-a) / (-b)`. It
is recommended that a linter warns whenever a
unary minus is encountered that has a
non-trivial `term` or `factor` as its operand.

text: A name can be one of four things:

bullets: ['A qualified name referring to either some object, a component\n(in a record) or field (in a tuple), or an enumeration type.', 'A tuple field or enumeration literal.', 'An index into an array.', 'A (builtin) function call.']

bnf: name ::= qualified_name
| name '.' IDENTIFIER
| name '[' expression ']'
| name '(' parameter_list ')'

parameter_list ::= expression { ',' expression }

text: The `qualified_name` must resolve to record component or
tuple field in scope, or a visible record
object, or a visible enumeration type.

text: If the prefix of a dot (`.`) access resolves to an
enumeration type, then the identifier must be
a valid literal of that type. If the prefix of
a dot (`.`) access resolves to a tuple, then
the identifier must be a valid field of the
type of that tuple. Any other prefix is an
error.

text: The type of the `name` in an array indexing prefix (i.e. `[`
.. `]`) must be an array type.

text: The `name` in a function call must resolve to one of the
builtin functions.

text: The builtin function `len` is of arity 1. Its parameter must
be of type `String` or an array type. Its
return type is `Integer`.

text: The builtin functions `startswith` and `endswith` are of
arity 2. All of their parameters must be of
type `String`. The return type of either
function is `Boolean`.

text: The builtin function `matches` is of arity 2. Its parameters
must be of type `String`. The return type is
`Boolean`. The second parameter must be a
valid regular expression. *(It is
implementation defined which regular
expression language is used, but it is highly,
_highly_ recommended to implement the standard
POSIX regular expressions.)*

text: In addition, the second parameter to the `matches` function
must be a static compile-time constant,
i.e. it must not depend on the value of a
record field or the value of a quantified
variable.

text: The numeric type conversion functions are of arity 1 and
polymorphic (they are defined for both integer and
rationals). They return the type indicated by the function
name. *(They are polymorphic in case we want to introduce
a true rational type, or a floating point type.)*

text: The `len` function computes the length of the given string
or array.

text: The `startswith` function returns true iff the first
parameter fully contains the second parameter
at its start.

text: The `endswith` function returns true iff the first parameter
fully contains the second parameter at its
end.

text: The `matches` function returns true iff the first parameter
is matched by the regular expression given in
the second parameter.

text: The `oneof` function returns true iff exactly one of its
parameters is true, and all others are false.

text: The `Integer` type conversion rounds to the nearest
integral, away from zero in the case of ties.

text: The `Decimal` type conversion simply converts
the given integer to the exact same rational.

bnf: quantified_expression ::=
'(' quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>'
expression_PREDICATE ')'

quantifier ::= 'forall' | 'exists'

text: The component name must be defined in the current record,
and must be an array type.

text: A quantified expression introduces a new name, that is valid
only inside the predicate. This new name must
not shadow any other. *(This means two
separate quantified expressions may use the
same name, but you may not nest and shadow,
and you may not shadow a component name
either.)*

text: The type of the predicate must be Boolean. The result of a
quantified expression is Boolean.

text: For universal *(forall)* quantification the final value is
true iff all predicates evaluate to
true. *(This means universal quantification
over an empty array is vacuously true.)*

text: For existential *(exists)* quantification the final value is
true iff the predicate evaluate to true at
least once. *(This means existential
quantification over an empty array is
vacuously false.)*

bnf: conditional_expression ::=
'if' expression_CONDITION 'then' expression_DEPENDENT
{'elsif' expression_CONDITION 'then' expression_DEPENDENT }
'else' expression_DEPENDENT

text: The condition expressions must be of Boolean type. The
dependent expressions must all be of the same
type, and the type of the entire conditional
expression is also of that type.

text: Each condition is evaluated in sequence. Evaluation stops on
the first condition that evaluates to true;
after which the corresponding dependent
expression is evaluated and returned.

text: If all conditions are evaluated to false, then the else
dependent expression is evaluated and
returned.

text: A `.trlc` file is simply a set of record object declarations.

bnf: trlc_file ::= file_preamble
{ trlc_entry }

trlc_entry ::= section_declaration
| record_object_declaration

text: It is permitted to indicate a package that has
not been declared in an `.rsl` file, in which
case it is declared by the
package_indication in the `.trlc` file. Such a package is
declared late. If two `.trlc` files declare the same
package, then it is unspecified which file actually
declares it.

text: A section has no semantic impact, and no impact on name
resolution. Section names do not have to be
unique. It may be exposed in an API, for
example to section a HTML view of
requirements.

bnf: section_declaration ::= 'section' STRING_section_name
'{' { trlc_entry } '}'

bnf: record_object_declaration ::=
qualified_name_RECORD_TYPE IDENTIFIER_object_name
'{' { component_association } '}'

component_association ::= IDENTIFIER_component_name '=' value

value ::= [ adding_operator ] INTEGER
| [ adding_operator ] DECIMAL
| STRING
| qualified_name_RECORD_OBJECT
| qualified_name_ENUM_TYPE '.' IDENTIFIER_enumeration_literal
| array_aggregate
| tuple_aggregate

array_aggregate ::= '[' [ value { ',' value } ] ']'

tuple_aggregate ::= '(' value { ',' value } ')'
| value { separator_symbol value }

text: The type of the declaration must be a valid, non-abstract
record type. If no qualified name is given, the record type
must be in the indicated package. *(Note that it is not
legal to declare a tuple object.)*

text: The name of the declaration must be a unique name and
sufficiently distinct in the current
package. *(See name resolution for a
definition of sufficiently distinct.)* The
name of the declaration must not shadow a type
name or package.

text: Each component name must be a valid, non-frozen component
of the record type. It is an error to attempt to assign to
a frozen component *(even if the value assigned would be the
same value as it's frozen value)*.

text: Each enumeration must be a valid enumeration type in the
indicated (or qualified) package. Each
enumeration literal must be a valid literal of
the indicated enumeration in the prefix.

text: The type of each value must match each component or array
element type. Records are specified through
references *(there is no way to specify an
inline anonymous instance)*.

text: It is an error to not provide a value for a non-optional
component.

text: The aggregate of a tuple must use the correct form. A
tuple without separators uses the bracket syntax
(e.g. `(1, 2, 3)`, and a tuple with separators must
use the separator syntax (e.g. `12345@42`).

text: A tuple value for a tuple without separators must
contain one value, in order, for each of its fields.

text: A tuple value for a tuple with separators must
contain the separator symbols as indicated in the type,
in order. Optional fields and their preceding separator
may be omitted. Once an optional field has been omitted,
all following (optional) fields must also be omitted.

text: A record object declaration creates a new binding for a
record. The value of any frozen components is the value
provided in the freezing declaration. After references
are resolved, all applicable checks on the object, including
any checks for tuples, are evaluated in the context
of this binding.

text: It is an error to refer to a record by name that does not
exist. It is legal to refer to an record that
has not been encountered yet, as references
are resolved after parsing.

text: A record reference must match in type, i.e. be of the
correct type or any record extension of that
type. *(For example if RE extends R, then a
list of R may contain references to instances
of R and RE. A list of RE may not contain any
references to R.)*

text: A value can be assigned to a component of a record object
only once.

text: When declaring record objects there are wider rules that
indicate name clashes. Specifically a record
may not be declared if its "simplified name"
clashes with any other "simplified name". A
"simplified name" is the name converted to
lowercase and all underscores removed.

text: A `Markup_String` allows you to inline references to TRLC
record in a string. The format is limited and
simple: any name or comma-separated list of
names enclosed in double square brackets
(i.e. `[[` and `]]`) is considered a
reference.

text: Attempting to nest, or close a list that does not exist, or
not close an open list before the end of the
string is an error.

text: The fragment of BNF grammar applicable is
qualified_name. The type of each named object
must be a record type. *(This means you cannot
reference types or enumerations.)*

text: The references are resolved late, just like an ordinary
record reference. *(This means you can
forward-reference objects, or reference
yourself.)*

text: The name resolution rules for the qualified_name are exactly
the same as they are for any other
qualified_name. *(This means you need to
import all packages from which you reference
objects.)*

text: The literal null value is only permitted to appear in
an equality or inequality. Any other context (such as
`(if a then null else b)` is rejected statically.

text: The expression `null == null` is statically true.

text: The value of an optional component or field that is
not specified is `null`.

text: For any other operator or operation, the null value is
considered out of bounds and raises an
error. *(This means you can check if something
is null or not, but any other use will cause
an error.)*