Next: , Previous: , Up: Types and Expressions   [Contents][Index]

10.3.4 subint

The integer type is available in Dezyne in a restricted way14: only a finite contiguous subrange of integer numbers can be used. An explicit type definition is needed for each subset, where a C-like syntax is used.

subint  ::= "subint" identifier "{" range "}" ";"
range   ::= integer ".." integer
integer ::= ("-")? [0-9]+

An example:

subint int {-1..2};

where subint is a keyword. This defines the finite type int with possible values -1, 0, 1, and 2. Available integer operators are:

i1 <= i2
i1 >= i2
i1 > i2
i1 == i2
i1 != i2
i1 + i2,

Integer addition,

i1 - i2

Integer subtraction,

where i1 and i2 denote integers.

note: Integers of different subint types can be used in comparison, assignment, and function calls. The verifier will check that the resulting integer value is within the defined subint range.



the subint definition allows range checking and prevents accidental unboundedness during model checking