XBNF
forall-construct -to -rule
to to **is ** FORALL forall-header
forall-body-stmt
[ forall-body-stmt ] ...
END FORALL

forall-body-stmt -to -rule
to to **is ** forall-assignment
-to **or ** where-stmt
-to **or ** where-construct
-to **or ** forall-stmt
-to **or ** forall-construct
XBNF

- Any procedure referenced in a
*forall-body-stmt*, including one referenced by a defined operation or assignment, must be pure as defined in Section . - If a
*forall-stmt*or*forall-construct*is nested in a*forall-construct*, then the inner`FORALL`may not redefine any*index-name*used in the outer*forall-construct*.

Thu Dec 8 16:17:11 CST 1994