1 Introduction¶
The reference establishes the core grammar of the language and its semantic rules. If you are not familiar with the language concepts, you may visit 2 Materials first to get introduced to the vocabulary.
Even thought this section is meant to be a rigorous language specification, it is progressive in order to easily explain each element of the grammar using what was already defined.
You can find it useful to have a precise information on the meaning of a particular syntax you encountered. The examples given here are valid and illustrate the correct syntax.
For each language construct presented a syntax template is provided. The templates consist on the comprehensive specification of the language.
Each template figures elements such as <some_label>, these must be replaced with the language
construct corresponding to the given label.
2 Links¶
A link is a reference to a identifier already defined in the code.
Syntax:
{<quantity>}
"""refer to {my_target_quantity}"""
Note
Links are resolved during semantic verification.
Links can only be present in 3.3 Block comment and 5.3 Constraint
3 Comment¶
A comment is a primitive composed of plain text. The comments allows to provide additional information to be included during 2.1.4 Document generation.
3.1 Tags¶
A tag is a user-defined identifier suffixed with @ which can be featured in a 3.3 Block comment.
Syntax:
@<identifier> <text>
"""
@rationale This quantity is meat to ...
@remark Note that ...
@desc Defines the quantity of ...
"""
3.2 Inline comment¶
An inline comment is a comment line that can be inserted at any place in the code.
Syntax:
# <text>
# This is an inline comment.
Note
Inline comments are ignored during document generation.
3.3 Block comment¶
A block comment is a multi-line comment that applies to the first element below the comment.
Syntax:
"""<text|link|tag>"""
"""
@useful something useful...
represents the principal car of the {system.user}.
"""
define car: Car;
4 Literals¶
A literals is a built-in language element that allows to specify the most basic language expression, the constants.
Literals can be used to build 2.1.2 State constraint.
Note
Literals can be compared to programming language literals;
Literals are of arbitrary precision and size;
Literals do not have a type but are constant 5 Quantity.
4.1 Strings¶
A string literal is an immutable character string provided with a given encoding format.
4.1.1 Character strings¶
A character string is a plain text string composed of printable and escape ASCII characters.
Syntax:
<format>'<text>'
'This is a string literal'
'This is a string\nliteral'
utf8'This is a string literal'
Note
Only alphanumeric, blanks and escape characters are allowed.
Only single quoted string are admissible
Strings cannot contain links
4.1.2 Digit strings¶
A digit string is a string that encodes a number in a given numerical basis.
The list of characters corresponding to the domain are implicitly ordered in ASCII order, starting to 0.
Syntax:
<basis>'<digits>'
h'ff0011'
b'000100'
o'002727'
Note
Only octal, binary and hexadecimal digit list are allowed
4.2 Numerics¶
4.2.2 Integer¶
An integer literal is a numerical token expressing a signed integer number.
Syntax:
[<sign>]<digits>
122331313
-1333
4.2.3 Rational¶
A rational literal is a numerical token expressing a rational number.
Syntax:
[<sign>]<digits>//<digits>
1223//4424
-3//4
Note
No spaces are allowed around the // symbol.
4.2.4 Decimal¶
A decimal literal is a numerical token expressing a decimal number.
Syntax:
[<sign>]<digits>[.<digits>][e[<sign>]<digits>]
1500.75
23e6
1e-6
-1.75
-2.
Note
The count of significant digits must be correct.
No spaces are allowed around the
esymbol.
4.2.5 Special¶
A special number literal is a literal token reserved for mathematical constants such as pi, or Euler’s number.
PI
EULER
IM
5 Quantity¶
A quantity is a component of the state defined in the 2.1.1 Functional specification.
A quantity is expected to belong to a certain domain via a 5.3 Constraint.
The general syntax to define a quantity is the following:
Syntax:
define <modifier> <identifier> [: <constraint> <constraint> ...]
define status: integer [[ = 0 ]];
define input temperature: real;
define output message; # belongs to any
Note
If no constraint is specified the quantity implicitly belongs to
anyQuantities can also be domains and there it is possible to write
define q1: q2
5.1 Explanations¶
The most simple example for a state constraint is the equality between quantities:
define sensor_temperature: real;
define cabin_temperature: [[ = sensor_temperature ]];
In the above example we can observe that:
cabin_temperatureis constrained to be equal to thesensor_temperature;cabin_temperatureimplicitly belongs to the singdefineon set composed ofsensor_temperature.
Note
The above syntax is especially convenient for simple constraints
Complex constraints should be expressed using 6.3 Requirement
5.2 Modifier¶
The quantity modifiers are statements about the scope of a certain quantity, they allow to differentiate between internals and external system state components.
Syntax:
[constant] [input|output|buffer]
define input sensor_temperature: real;
define output cabin_temperature: real;
5.3 Constraint¶
A constraint is an assertion about a certain quantity restricting its domain of belonging. A constraint can itself be seen as a domain, which is the domain of validity of the constraint.
These can be listed by separating each constraint with a blank. Doing so is equivalent to require that each constraint is met during verification.
define input sensor_temperature: real [[ > 10 ]];
5.3.1 Domain¶
The domains constraint are the most simple form of constraints. These assert that a quantity belongs to a previously defined domain.
define issue_point: PointBlades
5.3.1.1 Builtin¶
The language provide builtin domains such as real, integer, …
Syntax:
boolean|integer|rational|decimal|real|complex|empty|any
define friction_area: real;
define current: complex;
5.3.1.2 Explicit¶
An explicit domain is an explicit enumeration of primitives composing the domain. These primitives must be heterogeneous.
Syntax:
(( <literal>, <literal>, ... ))
define Spin: (( 'Up', 'Down', 'Strange' ));
define Opcode: (( h'ff00', h'ff01', h'ff02' ));
define Temperature: (( 90.0, 110, 200 ));
5.3.1.3 Intervals¶
An interval is a continuous part of a straight. It correspond to the notion of mathematical intervals.
Syntax:
<<|>> <real>:<real> <<|>>
define OneOne: <<-1:1>>;
define ExclOneOne: >>-1.:1.>>;
5.3.1.4 Product¶
The product matches the mathematical cartesian product.
Syntax:
<domain> * <domain> * ...
define RealPair: real * real;
define Rectangle: <<-1:1>> * <<0:2>>;
5.3.1.5 Union¶
The union matches the mathematical union binary operator.
Syntax:
<domain> || <domain> || ...
define NotZero: <<-1:0<< || >>0:1>>;
define MinusOneTwo: <<-1:1>> || <<0:2>>;
5.3.1.6 Intersection¶
The intersection matches the mathematical intersection binary operator.
Syntax:
<domain> && <domain> && ...
define Empty: <<-1:0<< && >>0:1>>;
define ZeroOne: <<-1:1>> && <<0:2>>;
5.3.2 Algebraical¶
An algebraical domain is a 5.3.1 Domain that is provided with an additional algebraical structure. It can be a vector or tensor space, or any user-defined algebraical construct.
Syntax:
<identifier> <arguments> (<domain>)
define position: vector<2>(real);
define multi_pole: matrix<12, 12>(complex);
define metric_tensor: tensor<3, -3>(real);
Note
Elements of numeric domain can be featured in algebraical expressions;
identifiermust match a previously defined structure constructor.
5.3.2.1 Arguments¶
The arguments of an algebraical are “template” parameters are passed to the structure to specify numerical information on the algebraical structure:
dimension, tuple representing the mathematical dimension
variance, dimension with signed indexes to specify the tensor variance
degrees, such as polynomial or Galois fields degrees
Syntax:
<integer, integer, ...>
5.3.2.2 Scalar¶
A scalar is a quantity constrained to be an algebraical of dimension 1.
define light_status: boolean;
define score: integer;
define pizza_slice: rational;
define plane_distance: real;
define electric_current: complex;
Note
Scalar algebras are the canonical ones by default
5.3.2.3 Vector¶
A vector is a quantity constrained to belong to a finite dimension vector space.
define buffer_state: vector<256>(boolean);
define car_speed: vector<2>(real);
define quad_speed: vector<4>(complex);
Note
components can be indexed by only one natural number.
5.3.2.4 Matrix¶
A matrix is a quantity constrained to belong to a finite dimension matrix space.
define probability_matrix: matrix<40, 60>(real);
define inertia_matrix: matrix<3>(real); # square matrix
5.3.2.5 Tensor¶
A tensor is a quantity constrained to belong to a finite dimension tensor space.
define quad_speed: tensor<4>(complex);
define metric_tensor: tensor<4, 4>(complex);
define curvature_tensor: tensor<4, -4, -4, -4>(complex);
Note
Matrices and vectors are special kind of tensors providing more algebraical features.
Indices signs stands for the variance of the tensor.
5.3.3 Blocks¶
A block constraint is an expression block that produces a constraint.
A constraint block can be expressed in a mathematical, algorithmic or semantic way.
Blocks are formally checked during 2.1.3 System verification.
Note
Constraint blocks can make usage of any previously defined quantity.
5.3.3.1 Semantic¶
A semantic block is similar to a 3.3 Block comment but is used to textually specify a constraint.
Syntax:
""<text|link>""
define good_slices:
""
equal to the {pizza_slices} such that ...
"";
Note
Semantic blocks are convenient for systems that do not require formal behavior validation.
5.3.3.2 Algorithmic¶
An algorithmic block is an expression block that allows to define an algorithm and therefore programmatically specify a constraint.
Syntax:
{{
<instruction>;
<instruction>;
...
<operator> <expression>
}}
define good_slices:
{{
let a = pizza_slices;
let b;
b = 2 * a;
a += b;
= (b + a) * 5
}};
Note
Algorithmic blocks are convenient for systems that require a formal validation simpler than a formal proof.
5.3.3.3 Mathematic¶
A mathematic block is an expression block that allows to define literal variables and use mathematical language to state properties about the variables.
A mathematical constraint allows to define
Syntax:
[[
<expression>;
<expression>;
...
<operator> <expression>
]]
define good_slices:
[[
let a = pizza_slices + b;
let b = 2 * a;
= (b + a) * 5
]];
In the above example, the existence of a and b is verified during system verification.
Note
Mathematic blocks are convenient for systems that require a mathematical validation of behavior.
5.4 Function¶
A function is analogous to a mathematical function. It is a special quantity belonging to a functional domain.
Functions can be used to define relationships between input and output quantities.
A function can be defined using the keyword function:
Syntax:
function <identifier>(<parameter>, <parameter>, ...)
[: <constraint> <constraint> ... ;]
function euclidean_distance(
x: vector<2>(real);
y: vector<2>(real);
):
real [[ = ((x - y) ^ 2) ^ (1//2) ]];
Functions can take parameters and specifies a template constraint. The parameters can latter be specified to instantiate the constraint.
Note
Constraint blocks of a function can make usage of the provided parameters.
6 Components¶
The components are the elementary building blocks of the func language.
Components are all gathered in a source file consists on a system as defined in 2.1.1 Functional specification.
Components can be provided with a block comment immediately above the component definition.
Syntax:
<block|quantity|requirement>
Note
A system can contain multiple sub-systems. Therefore:
Sources files can be included within each other
The language must be provided a component that can embed components
6.1 Block¶
A block is the base container for other components of the language. Blocks can be nested, a block can contain any component.
Syntax:
block {
<component>
<component>
...
}
block car_control {
# ...
block car_dynamics {
# ...
}
# ...
}
6.1.1 Scope¶
The components that are in scope of a block are:
The components of the parent block
The components explicitly imported
If a component is not in scope of a block, then it will not be possible reference inside the block.
In particular, if a quantity is not in scope, it will not be possible to import it in constraints.
A block can be brought in scope using the keyword import.
Syntax:
import <identifier> [as <alias>]
block mozzarella {
# ...
}
block pizza {
import mozzarella
# ...
}
Note
If no root block is provided within a source file, then components are considered inside a default root block named after the file name of the source.
6.2 Quantity¶
A quantity is defined as specified in 5 Quantity. All the quantities under a block form the state of the block.
Quantities can be gathered in more complex structures using the {} notation:
Syntax:
define <identifier> {
[<identifier>[: <constraint> <constraint> ...];]
[<identifier>[: <constraint> <constraint> ...];]
...
}
This notation provides syntactic sugar to build quantities with labeled field structure.element.
define Car {
position: vector<2>(real);
speed: vector<2>(real);
direction: Direction;
}
6.3 Requirement¶
A requirement is a labeled constraint, it is syntactic sugar meant to postpone the constriction of a quantity by labeling a list a constraints that applies to that quantity.
Syntax:
require <identifier> on <quantity>: <constraint> [<constraint> ...];
require object_distance on distance_to_target:
[[
> minimal_distance_to_target
]]
[[
= euclidean_distance(object.position, target.position)
]];
If a quantity is immediately constrained during its definition as saw in 5 Quantity, then way say the quantity is anonymously constrained.