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?

  • $\begingroup$ Maybe my browser isn't rendering well, but I don't see that symbol on the Wikipedia page. Did you quote from some other source? $\endgroup$ Jan 30, 2020 at 12:52


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.