Rodin User’s Handbook v.2.8: About the notation that we use

3.2.1 About the notation that we use

We denote a sequence of identifiers with $\mathbf{x} = x_1,\ldots ,x_ n$ and $\mathbf{x}’ = x’_1,\ldots ,x’_ n$ . As a convention, we use

$\mathbf{c}$ for constants
$\mathbf{v}$ and $\mathbf{w}$ for variables of an abstract or a concrete machine respectively
$\mathbf{t}$ and $\mathbf{u}$ for parameters of an abstract or concrete machine respectively
$A$ for axioms
$I$ and $J$ for the invariants of the abstract machines or concrete machine respectively
$G$ and $H$ for the guards of the abstract events or concrete event respectively