Parsing

Parsing

It was a mistake not to make the syntax 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.