Explicit universal quantifier. It consists of one or more variables (Var), each optionally surrounded by a declare role, followed by a logical formula (optionally surrounded by a formula role). (See: quantifier module)

(n.) A programming construct that specifies a set of loop iterations and further specifies that these iterations can be done in any order. data parallel and shared variable programs are often expressed using forall loops.