A WITH statement has the form:
WITH id = e DO S END
where id is an identifier, e an expression,
and S a statement.
The statement declares id with scope S as an
alias for the variable e or as a readonly name for
the value e. The expression e is evaluated once, at entry
to the WITH statement.
The statement is like the procedure call P(e), where P is declared as:
PROCEDURE P(mode id: type of e) = BEGIN S END P;
If e is a
writable designator,
mode is VAR; otherwise,
mode is READONLY.
The only difference
between the WITH statement and the call P(e) is that free
variables, RETURNs, and EXITs that occur in the WITH
statement are interpreted in the context of the WITH statement,
not in the context of P.
A single WITH can contain multiple bindings, which are evaluated sequentially. That is:
WITH id_1 = e_1, id_2 = e_2, ...
is equivalent to:
WITH id_1 = e_1 DO
WITH id_2 = e_2 DO ....