state formula

A state formula’s free variables range over the program variables, and denote a set of state

Or: a state formula is basically a predicate over program variables.