The following diagram illustrates the hierarchy of numeric types supported by Caesar.
An arrow from a type to another type indicates that it is a subtype and that a value can be converted into the supertype. This is done automatically by Caesar when appropriate.
Mathematical Number Types
Caesar supports various number types that are not restricted by a finite bit size. Therefore, all of these types have infinitely many values.
Unsigned integers, i.e. values
2, and so on.
Unsigned real numbers, i.e. values x ∈ ℝ such that x ≥ 0.
This is the type of fraction expressions
b are unsigned integer literals, as well as decimals such as
Actual real numbers!
Extended unsigned real numbers.
This type includes all values from the
UReal type and also allows the value
This type admits a Heyting algebra and can be used as a verification domain.This type was previously called
Realplus. For the moment, Caesar also accepts this name.