Type Relations

By looking at the expressions occurring in statements, an equivalence relation between primitive types can be inferred. The following cases are distinguished:

• For relational expressions such as $v = u$ or $v \leq u$, an equivalence between $T_v$ and $T_u$ is inferred.
• For arithmetic expression such as $v+u$ or $v*u$, an equivalence between $T_u$ and $T_v$ is inferred.
• For two different array accesses $a[v]$ and $a[u]$ an equivalence between $T_v$ and $T_u$ is inferred.
• From an assignment $v := u$ we infer that $T_u$ is a subtype of $T_v$,

By type, we will generally mean an equivalence class of primitive types. Subtyping is important to avoid the problem of pollution, the derivation of counter-intuitive equivalences due to commutativity and transitivity of the equivalence relation [22].