SUBSET(S)
,
with the parentheses required.
Not requiring the parentheses allows you to write
SUBSET S \cup T
.
Don't. People reading your algorithm won't
know if it means
SUBSET (S \cup T)
or
(SUBSET S) \cup T
.
I had to try it to find out which it is.
TLA+ has 76 infix operators, most of them user-definable, as well
as a dozen prefix and postfix operators. It's impossible to
define the precedence of those operators to satisfy everyone.
How should a + b $ c
be parsed? (The operator
$
is user-definable.)
In TLA+, operator precedence is a partial ordering relation. The
expression a + b $ c
is syntactically incorrect because
the precedence of +
is neither lower nor higher than that
of $
. In general, numerical-valued operators have
higher precedence (bind more tightly) than set-valued operators, which
have higher precedence than Boolean-valued operators. The
operators of propositional logic have lowest precedence.
The precedence of user-definable operators is based on how I thought
they were likely to be used.
Boolean-valued operators
have lower precedence than (don't bind as tightly as) other operators.
The precise definition of precedences can be found in the nine-page Summary of TLA+. But you and readers of your algorithms shouldn't have to worry about that. Just use parentheses if it's not obvious how an expression is parsed.