Arithmetic
Naturals
The most basic type of number in Vehicle are the natural numbers.
The type of natural numbers is written as Nat
.
The available operations over naturals are:
Operation |
Symbol |
Type |
Example |
---|---|---|---|
Addition |
|
|
|
Multiplication |
|
|
|
Division |
|
|
|
Less than or equal |
|
|
|
Less than |
|
|
|
Greater than or equal |
|
|
|
Greater than |
|
|
|
Note that inequalities can be chained, so that x < y <= z
will be
expanded to x < y and y <= z
.
Rationals
Rational numbers in Vehicle are stored using arbitrary precision.
The type of rational numbers is written as Rat
.
The available operations over rationals are:
Operation |
Symbol |
Type |
Example |
---|---|---|---|
Addition |
|
|
|
Subtraction |
|
|
|
Multiplication |
|
|
|
Division |
|
|
|
Negation |
|
|
|
Less than or equal |
|
|
|
Less than |
|
|
|
Greater than or equal |
|
|
|
Greater than |
|
|
|
Note
We are aware that the disconnect between the semantics of rational/real numbers and floating point can lead to soundness bugs in verification. Adding floating point types with configurable precision is on our road map.