"The notation is mainly ALGOL-like and requires
little explanation. To distinguish references to the
value of a function before calling the specified function
from references to its value after the call, we enclose
the old or previous value in single quotes (e.g. 'VAL').
If the value does not change, the quotes are optional.
Brackets ("[" and "]") are used to indicate the scope
of quantifiers. "=" is the relation "equals" and not
the assignment operator as in FORTRAN."
The code therein uses the specification language described in https://dl.acm.org/doi/pdf/10.1145/355602.361309 (reference [3] in the 1972 paper). From there:
"The notation is mainly ALGOL-like and requires little explanation. To distinguish references to the value of a function before calling the specified function from references to its value after the call, we enclose the old or previous value in single quotes (e.g. 'VAL'). If the value does not change, the quotes are optional. Brackets ("[" and "]") are used to indicate the scope of quantifiers. "=" is the relation "equals" and not the assignment operator as in FORTRAN."