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$ – Carl Witthoft Jan 30 '20 at 12:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.