The 'square' subset symbols are sometimes used to express analogous concepts to subsets, like prefixes or suffixes.
However their use in CSP seems to be counterintuitive to their shape: $⊑$ appears analogous to $⊇$ (as opposed to the more similar looking $⊆$):
A process $P$ refines $Q$, denoted as $Q⊑_TP$, iff $traces(P) ⊆ traces(Q)$.
Does Hoare explain anywhere why he chose this orientation of the symbol?
