Skip to content

ESL0003 - Units

Field Value
Author(s) A.T. Hofkamp
Reviewer(s) T. Wilschut, T.J.L. Schuijbroek
Status Final
Type Standard (S)
Created 2019-11-26
Finalized 2019-12-04

Warning

This LEP's syntax enhancement is written using an EBNF syntax as opposed to the current PEG syntax since it was finalized before the switch.

Abstract

In designing physical systems, using correct physical domains and units for variables in the system is of utmost importance. ESL allows associating a unit with a literal value when comparing a variable with a bound, there is no support for verifying if the unit is compatible with the used variable.

This LEP addresses that gap by attaching allowed units to a variable through its type, thus allowing correctness verification of the comparisons with respect to the used units.

Motivation

ESL can associate units with literal values, but variables have no notions of domain or unit, making it impossible to verify whether a comparison between a variable and a literal value, or between two variables makes any sense. This LEP proposes to extend the type system with units to enable checking that.

Rationale

Physical quantities in a system have a domain, for example they express speed or distance. Such quantities are represented by variables in an ESL specification. In current ESL, domains can already be expressed as a type, for example

1
2
3
4
5
6
define type
  speed is a real

world
  variable
    s is a speed

Here variable s has type speed, and can assume real values in the system.

Note that while it looks like physical domains have been added, there is actually no real change in ESL here. Type speed is a normal type definition already available in ESL, the type just has a suggestive name. By introducing such type names for physical domains in the specification and using them consistently, a large step towards clear specifications can be made already.

Types with units

Within a physical domain, several different units of measurement typically exist. For example, distance may be expressed in meter ([m]), nano-meter ([nm]), or light year ([ly]) depending on the field. Such units are used to unambiguously state physical quantities. In ESL, such quantities are used as boundary values for variables.

Often, a unit is narrowly connected to a domain. For example, using the unit [m/s] implies that the value expresses a speed. Attaching allowed units to a domain in ESL formalizes this relation, and enables checking that a range restriction in a constraint or requirement makes sense with respect to the domain of the variable.

For this reason, this LEP proposes to extend types in ESL with a list of allowed units as follows

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
define type
  speed is a real with units m/s, km/h

 world
  variables
    s is a speed

  design-constraint
    gl1: s must be at most 5 [km/h]
    gl2: s should be at least 0.1 [m/s]

Again s is a variable of type speed, but now the specification also lists the units m/s and km/h that should be used in the speed domain.

Conceptually, the idea is that units define how a variable of a given type can communicate with its environment. That is, by adding the [km/h] unit to type speed, variables of that type can give and accept values with that unit. Comparisons described in the design constraint of the example are one spot where such communication occurs as demonstrated in constraint gl1.

Allowing a variable to communicate in several different units is not a problem, as long as it is always clear which unit is being used. In ESL, that information is stated with the literal value. Constraint gl2 shows an example. From a project point of view it may be undesirable to have more than one unit in a domain. Such a concern can be addressed in ESL by specifying exactly one unit with a type.

Extending types

Extending a type with units copies the units as well. You cannot remove units (except for the dimensionless unit, as discussed below), but new units may be added. An example is

1
2
3
4
5
define type
  distance with units m
  travel-distance is a distance with unit km
  cycle-distance is a travel-distance
  information is a boolean

The distance domain only has unit m, while both the travel-distance domain and the cycle-distance domain have units m as well as km.

The types that have no unit listed directly or indirectly like information in the example use the dimensionless unit [-] to exchange values with their environment. Similarly, literal values without stated dimension are also assumed to be dimensionless.

To avoid that the dimensionless unit is available in every type (and thus defeating the whole idea of using units for correctness checking of comparisons), the implicitly added dimensionless unit is removed as soon as units are added to a type.

Comparing variables and literal values

Above it was already explained that in a comparison between a variable and a literal value the latter must have a unit listed with the type of the former. Types without specified units get unit [-], which thus forbids the option of comparing a variable with a type with units and a literal value without unit or vice versa.

Some examples of correct and incorrect comparisons are shown below

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
define type
  speed is a real with units m/s, km/h

world
  variables
    s is a speed
    b is a boolean

  design-constraint
    gl1: s must be at most 5 [km/h]     # Ok
    gl2: s should be at least 0.1 [m/s] # Ok
    gl3: b should be equal to false     # Ok, [-] implied
    gl4: b should be equal to true [-]  # Ok

    sl1: s may be less than 1 [m/h]    # ERROR, [m/h] is not allowed
    sl2: s may be less than 100        # ERROR, [-] is not allowed
    sl3: b can be equal to true [km/h] # ERROR, [km/h] is not allowed

The constraints gl1 and gl2 are correct, as the units km/h and m/s are both associated with the type speed of variable s. In gl3, the boolean type has no units listed, meaning it can exchange dimensionless values only. The literal value false has no unit listed either, it is a dimensionless value. Constraint gl4 is equivalent to gl3, except the literal value true does have its lack of dimension stated explicitly.

Trying to exchange values without common unit fails. In constraints sl1 and sl2, units m/h respectively - of the literal values are both not in the list of units of type speed. Similarly, in sl3, a dimensionless variable cannot take a literal value with unit [km/h].

For comparisons between variables the rule is that variables can be compared if they can exchange values with each other. That is, they must share at least one unit between their types. A few examples are shown below

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
define type
  travel-distance is a real with unit m, km
  measured-distance is a real with unit m, cm
  speed is a real with unit m/s

world
  variables
    r, t is a travel-distance
    m is a measured-distance
    s is a speed
    u, v is a real

  design-constraint
    vl1: r is less then t    # Ok
    vl2: u is equal to v     # Ok
    vl3: d is at least m     # Ok, [m] is common

    vl4: t is less than s    # Error, no common unit
    vl5: t is greater than u # Error, no common unit

In vl1 and vl2, variables with the same type are compared with each other. This is always allowed as they trivially share at least one unit. In vl3 a variable of type travel-distance is compared with a variable of type measured-distance. This is allowed as they share unit [m].

Constraint vl4 is incorrect, as variable t can be converted to units [m] and [km], while variable s can only be converted to unit [m/s]. Constraint vl5 is wrong as variable u can only be converted to dimensionless unit [-], which is not a unit of variable t.

Specification

The LEP introduces new syntax for attaching units to types, and additional checks on correctness when exchanging values with variables. The rules about the latter part have been explained above. Here, the new syntax is defined.

The option of attaching a list of units to a type within a type definition section requires extension of the type-definition rule in the ESL syntax. The result is shown below.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
type-definition ::=
    "define" "type" \n
  { new-type-name [ unit-specification ] \n }+

new-type-name ::=
    TYPE-NAME
  | TYPE-NAME "is" ( "a" | "an" ) TYPE-NAME

unit-specification ::=
    "with" ( "unit" | "units" ) UNIT { "," UNIT }

The type-definition rule has been refactored, introducing the new-type-name rule without changing the syntax. As before, it either creates a new type name from scratch using the TYPE-NAME line, or it creates a new type name as a variant of an existing type using the [TYPE-NAME "is" ( "a" | "an" ) TYPE-NAME] line.

The addition proposed by this LEP is in the new unit specification unit-specification rule, allowing to attach unit names to a type.

Backwards Compatibility

Currently all ESL specifications have no units attached to variables. Thus, all variables have implied dimensionless unit [-]. Literal values may have units listed in comparisons. A specification that has any unit other than [-] associated with a value will be flagged as invalid.

This problem can be solved by either adding proper lists of allowed units to the types, or by removing units from the literal values.

Security implications

The LEP proposes additional checks only. These checks are not computation intense. It does not seem likely an attacker could easily exploit units.

How to teach this

A user needs to understand

  1. A variable expressing a physical value in a system has a domain. A domain is expressed as a type in ESL.
  2. A domain has one or more valid units for values in its domain.
  3. A type can be given units, enabling exchange of values in those units.
  4. You can compare a variable with either a literal value with a correct unit, or with variables that share at least one unit.

Proof of concept

Currently there is no proof of concept available.

Rejected ideas

No ideas were rejected until now.

Open issues

As variables have no well-defined unit, relations implemented in programming language cannot quite deal with such values.

For feasibility studies, using different units in a specification implies that at some point a conversion to a common unit must take place, or sanity of bounds expressed in different units cannot be decided. For example, in the above example, the question whether s has a solution while complying with constraints sl1 and sl2 means a conversion between m/s and km/h must be done.

References

No external references exist yet.